let g1, g2 be Ordinal-Sequence-valued Sequence; :: thesis:
assume A1: dom g1 = dom g2 ; :: thesis:
assume A2: dom g1 <> {} ; :: thesis:
assume A3: for a being Ordinal st a in dom g1 holds
g1 . a c= g2 . a ; :: thesis:
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;

let x, y be set ; :: thesis:
assume x in X ; :: thesis:
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:
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:
then A9: b c= a by A6, A8, ORDINAL1:16;
then A10: b in dom (g1 . 0) by A6, ORDINAL1:12;

end;

end;

X c= Z

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in X ; :: thesis:
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 ) ) ;

end;

end;