let g1, g2 be Ordinal-Sequence-valued Sequence; :: thesis: ( dom g1 = dom g2 & dom g1 <> {} & ( for a being Ordinal st a in dom g1 holds
g1 . a c= g2 . a ) implies criticals g1 c= criticals g2 )
assume A1: dom g1 = dom g2 ; :: thesis: ( not dom g1 <> {} or ex a being Ordinal st
( a in dom g1 & not g1 . a c= g2 . a ) or criticals g1 c= criticals g2 )
assume A2: dom g1 <> {} ; :: thesis: ( ex a being Ordinal st
( a in dom g1 & not g1 . a c= g2 . a ) or criticals g1 c= criticals g2 )
assume A3: for a being Ordinal st a in dom g1 holds
g1 . a c= g2 . a ; :: thesis: criticals g1 c= criticals g2
set f1 = g1 . 0;
set f2 = g2 . 0;
0 in dom g1 by A2, ORDINAL3:8;
then ( g1 . 0 c= g2 . 0 & g1 . 0 in rng g1 & g2 . 0 in rng g2 ) by A1, A3, FUNCT_1:def 3;
then A4: dom (g1 . 0) c= dom (g2 . 0) by GRFUNC_1:2;
set X = { a where a is Element of dom (g1 . 0) : ( a in dom (g1 . 0) & ( for f being Ordinal-Sequence st f in rng g1 holds
a is_a_fixpoint_of f ) ) } ;
set Z = { a where a is Element of dom (g2 . 0) : ( a in dom (g2 . 0) & ( for f being Ordinal-Sequence st f in rng g2 holds
a is_a_fixpoint_of f ) ) } ;
reconsider X = { a where a is Element of dom (g1 . 0) : ( a in dom (g1 . 0) & ( for f being Ordinal-Sequence st f in rng g1 holds
a is_a_fixpoint_of f ) ) } , Z = { a where a is Element of dom (g2 . 0) : ( a in dom (g2 . 0) & ( for f being Ordinal-Sequence st f in rng g2 holds
a is_a_fixpoint_of f ) ) } as ordinal-membered set by Th46;
set Y = Z \ X;

A5: now :: thesis: for x, y being set st x in X & y in Z \ X holds
x in y

let x, y be set ; :: thesis: ( x in X & y in Z \ X implies x in y )
assume x in X ; :: thesis: ( y in Z \ X implies x in y )
then consider a being Element of dom (g1 . 0) such that
A6: ( x = a & a in dom (g1 . 0) & ( for f being Ordinal-Sequence st f in rng g1 holds
a is_a_fixpoint_of f ) ) ;
assume y in Z \ X ; :: thesis: x in y
then A7: ( y in Z & not y in X ) by XBOOLE_0:def 5;
then consider b being Element of dom (g2 . 0) such that
A8: ( y = b & b in dom (g2 . 0) & ( for f being Ordinal-Sequence st f in rng g2 holds
b is_a_fixpoint_of f ) ) ;
assume not x in y ; :: thesis: contradiction
then A9: b c= a by A6, A8, ORDINAL1:16;
then A10: b in dom (g1 . 0) by A6, ORDINAL1:12;

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

let f be Ordinal-Sequence; :: thesis: ( f in rng g1 implies b is_a_fixpoint_of f )
assume A11: f in rng g1 ; :: thesis: b is_a_fixpoint_of f
then consider z being object such that
A12: ( z in dom g1 & f = g1 . z ) by FUNCT_1:def 3;
reconsider z = z as set by TARSKI:1;
A13: f c= g2 . z by A3, A12;
g2 . z in rng g2 by A1, A12, FUNCT_1:def 3;
then A14: b is_a_fixpoint_of g2 . z by A8;
a is_a_fixpoint_of f by A6, A11;
then a in dom f ;
then A15: b in dom f by A9, ORDINAL1:12;
then f . b = (g2 . z) . b by A13, GRFUNC_1:2
.= b by A14 ;
hence b is_a_fixpoint_of f by A15; :: thesis: verum

end;

hence contradiction by A7, A8, A10; :: thesis: verum

end;

X c= Z

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in Z )
assume x in X ; :: thesis: x in Z
then consider a being Element of dom (g1 . 0) such that
A16: ( x = a & a in dom (g1 . 0) & ( for f being Ordinal-Sequence st f in rng g1 holds
a is_a_fixpoint_of f ) ) ;

now :: thesis: for f being Ordinal-Sequence st f in rng g2 holds
a is_a_fixpoint_of f

let f be Ordinal-Sequence; :: thesis: ( f in rng g2 implies a is_a_fixpoint_of f )
assume f in rng g2 ; :: thesis: a is_a_fixpoint_of f
then consider z being object such that
A17: ( z in dom g2 & f = g2 . z ) by FUNCT_1:def 3;
reconsider z = z as set by TARSKI:1;
A18: g1 . z c= f by A1, A3, A17;
then A19: dom (g1 . z) c= dom f by GRFUNC_1:2;
g1 . z in rng g1 by A1, A17, FUNCT_1:def 3;
then a is_a_fixpoint_of g1 . z by A16;
then ( a in dom (g1 . z) & a = (g1 . z) . a ) ;
then ( a in dom f & a = f . a ) by A18, A19, GRFUNC_1:2;
hence a is_a_fixpoint_of f ; :: thesis: verum

end;

hence x in Z by A16, A4; :: thesis: verum

end;

then X \/ (Z \ X) = Z by XBOOLE_1:45;
then criticals g2 = (criticals g1) ^ (numbering (Z \ X)) by A5, Th25;
hence criticals g1 c= criticals g2 by Th9; :: thesis: verum