let b be ordinal number ; :: thesis: for g being Ordinal-Sequence-valued T-Sequence st dom g <> {} & ( for c being ordinal number st c in dom g holds
b is_a_fixpoint_of g . c ) holds
ex a being ordinal number st
( a in dom (criticals g) & b = (criticals g) . a )
let g be Ordinal-Sequence-valued T-Sequence; :: thesis: ( dom g <> {} & ( for c being ordinal number st c in dom g holds
b is_a_fixpoint_of g . c ) implies ex a being ordinal number 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 ThA1;
assume that
A0: dom g <> {} and
A1: for c being ordinal number st c in dom g holds
b is_a_fixpoint_of g . c ; :: thesis: ex a being ordinal number st
( a in dom (criticals g) & b = (criticals g) . a )
b is_a_fixpoint_of g . 0 by A1, A0, ORDINAL3:8;
then A2: b in dom (g . 0) by ABIAN:def 3;

now

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 set st
( x in dom g & f = g . x ) by FUNCT_1:def 3;
hence b is_a_fixpoint_of f by A1; :: thesis: verum

end;

then b in X by A2;
then b in rng (criticals g) by ThN1a;
then ex x being set st
( x in dom (criticals g) & b = (criticals g) . x ) by FUNCT_1:def 3;
hence ex a being ordinal number st
( a in dom (criticals g) & b = (criticals g) . a ) ; :: thesis: verum