fact: Definition cont_fun_th3_prop f b F := [/\ fgraph F, domain F = omega0 \times aleph1, (allf F ordinalp /\ forall i x, i <o omega0 -> b <o x -> x <o aleph1 -> Vg F (J i x) = \0o), forall i, i <o omega0 -> ocontinuous_below (fun x => (Vg F (J i x))) aleph1 & forall x, x <=o b -> olimit (fun i => (Vg F (J i x))) omega0 (f x)].
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)