let g1, g2 be Ordinal-Sequence-valued T-Sequence; :: thesis: ( dom g1 = dom g2 & dom g1 <> {} & ( for a being ordinal number st a in dom g1 holds
g1 . a c= g2 . a ) implies criticals g1 c= criticals g2 )
assume Z0: dom g1 = dom g2 ; :: thesis: ( not dom g1 <> {} or ex a being ordinal number st
( a in dom g1 & not g1 . a c= g2 . a ) or criticals g1 c= criticals g2 )
assume Z1: dom g1 <> {} ; :: thesis: ( ex a being ordinal number st
( a in dom g1 & not g1 . a c= g2 . a ) or criticals g1 c= criticals g2 )
assume Z2: for a being ordinal number 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 Z1, ORDINAL3:8;
then ( g1 . 0 c= g2 . 0 & g1 . 0 in rng g1 & g2 . 0 in rng g2 ) by Z0, Z2, FUNCT_1:def 3;
then Z4: 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 ThA1;
set Y = Z \ X;

A1: now

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
B1: ( 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 B2: ( y in Z & not y in X ) by XBOOLE_0:def 5;
then consider b being Element of dom (g2 . 0) such that
B3: ( 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 B4: b c= a by B1, B3, ORDINAL1:16;
then B5: b in dom (g1 . 0) by B1, ORDINAL1:12;

now

let f be Ordinal-Sequence; :: thesis: ( f in rng g1 implies b is_a_fixpoint_of f )
assume B7: f in rng g1 ; :: thesis: b is_a_fixpoint_of f
then consider z being set such that
B6: ( z in dom g1 & f = g1 . z ) by FUNCT_1:def 3;
B8: f c= g2 . z by Z2, B6;
g2 . z in rng g2 by Z0, B6, FUNCT_1:def 3;
then BB: b is_a_fixpoint_of g2 . z by B3;
a is_a_fixpoint_of f by B1, B7;
then a in dom f by ABIAN:def 3;
then B9: b in dom f by B4, ORDINAL1:12;
then f . b = (g2 . z) . b by B8, GRFUNC_1:2
.= b by BB, ABIAN:def 3 ;
hence b is_a_fixpoint_of f by B9, ABIAN:def 3; :: thesis: verum

end;

hence contradiction by B2, B3, B5; :: thesis: verum

end;

X c= Z

proof

let x be set ; :: 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
B1: ( 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

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 set such that
B4: ( z in dom g2 & f = g2 . z ) by FUNCT_1:def 3;
B5: g1 . z c= f by Z0, Z2, B4;
then B6: dom (g1 . z) c= dom f by GRFUNC_1:2;
g1 . z in rng g1 by Z0, B4, FUNCT_1:def 3;
then a is_a_fixpoint_of g1 . z by B1;
then ( a in dom (g1 . z) & a = (g1 . z) . a ) by ABIAN:def 3;
then ( a in dom f & a = f . a ) by B5, B6, GRFUNC_1:2;
hence a is_a_fixpoint_of f by ABIAN:def 3; :: thesis: verum

end;

hence x in Z by B1, Z4; :: thesis: verum

end;

then X \/ (Z \ X) = Z by XBOOLE_1:45;
then criticals g2 = (criticals g1) ^ (numbering (Z \ X)) by A1, ThN7;
hence criticals g1 c= criticals g2 by Lem4; :: thesis: verum