let b be Ordinal; :: thesis: for g being Ordinal-Sequence-valued Sequence st dom g <> {} & ( for c being Ordinal st c in dom g holds
b is_a_fixpoint_of g . c ) holds
ex a being Ordinal st
( a in dom (criticals g) & b = (criticals g) . a )
let g be Ordinal-Sequence-valued Sequence; :: thesis: ( dom g <> {} & ( for c being Ordinal st c in dom g holds
b is_a_fixpoint_of g . c ) implies ex a being Ordinal st
( a in dom (criticals g) & b = (criticals g) . a ) )
reconsider X = { a where a is Element of dom (g . 0) : ( a in dom (g . 0) & ( for f being Ordinal-Sequence st f in rng g holds
a is_a_fixpoint_of f ) ) } as ordinal-membered set by Th46;
assume that
A1: dom g <> {} and
A2: for c being Ordinal st c in dom g holds
b is_a_fixpoint_of g . c ; :: thesis: ex a being Ordinal st
( a in dom (criticals g) & b = (criticals g) . a )
b is_a_fixpoint_of g . 0 by A2, A1, ORDINAL3:8;
then A3: b in dom (g . 0) ;

now :: thesis: for f being Ordinal-Sequence st f in rng g holds
b is_a_fixpoint_of f

let f be Ordinal-Sequence; :: thesis: ( f in rng g implies b is_a_fixpoint_of f )
assume f in rng g ; :: thesis: b is_a_fixpoint_of f
then ex x being object st
( x in dom g & f = g . x ) by FUNCT_1:def 3;
hence b is_a_fixpoint_of f by A2; :: thesis: verum

end;

then b in X by A3;
then b in rng (criticals g) by Th19;
then ex x being object st
( x in dom (criticals g) & b = (criticals g) . x ) by FUNCT_1:def 3;
hence ex a being Ordinal st
( a in dom (criticals g) & b = (criticals g) . a ) ; :: thesis: verum