defpred S₁[ Ordinal] means ( $1 in F₁() implies F₃() . $1 = F₄() . $1 );
A4: for F being Ordinal st ( for G being Ordinal st G in F holds
S₁[G] ) holds
S₁[F]

proof

let B be Ordinal; :: thesis: ( ( for G being Ordinal st G in B holds
S₁[G] ) implies S₁[B] )
assume A5: for G being Ordinal st G in B holds
S₁[G] ; :: thesis: S₁[B]
assume A6: B in F₁() ; :: thesis: F₃() . B = F₄() . B
then consider S1B being ManySortedSet of F₂(B) such that
A7: ( F₃() . B = S1B & ( for x being object st x in F₂(B) holds
S1B . x = F₅(x,(F₃() | B)) ) ) by A2;
consider S2B being ManySortedSet of F₂(B) such that
A8: ( F₄() . B = S2B & ( for x being object st x in F₂(B) holds
S2B . x = F₅(x,(F₄() | B)) ) ) by A3, A6;
A9: ( dom S1B = F₂(B) & F₂(B) = dom S2B ) by PARTFUN1:def 2;
for x being object st x in F₂(B) holds
S1B . x = S2B . x

proof

let x be object ; :: thesis: ( x in F₂(B) implies S1B . x = S2B . x )
assume A10: x in F₂(B) ; :: thesis: S1B . x = S2B . x
( S1B <> {} & S2B <> {} ) by A10, A9;
then ( B in dom F₃() & B in dom F₄() ) by A7, A8, FUNCT_1:def 2;
then A11: ( dom (F₃() | B) = B & B = dom (F₄() | B) ) by RELAT_1:62, ORDINAL1:def 2;
for y being object st y in B holds
(F₃() | B) . y = (F₄() | B) . y

proof

let y be object ; :: thesis: ( y in B implies (F₃() | B) . y = (F₄() | B) . y )
assume A12: y in B ; :: thesis: (F₃() | B) . y = (F₄() | B) . y
then reconsider Y = y as Ordinal ;
A13: Y in F₁() by A12, A6, ORDINAL1:10;
thus (F₃() | B) . y = F₃() . Y by A12, FUNCT_1:49
.= F₄() . Y by A12, A5, A13
.= (F₄() | B) . y by A12, FUNCT_1:49 ; :: thesis: verum

end;

then A14: F₃() | B = F₄() | B by A11, FUNCT_1:2;
S1B . x = F₅(x,(F₃() | B)) by A10, A7;
hence S1B . x = S2B . x by A14, A10, A8; :: thesis: verum

end;

hence F₃() . B = F₄() . B by A7, A8, A9, FUNCT_1:2; :: thesis: verum

end;

A15: for F being Ordinal holds S₁[F] from ORDINAL1:sch 2(A4);
A16: ( dom (F₃() | F₁()) = F₁() & F₁() = dom (F₄() | F₁()) ) by A1, RELAT_1:62;
for y being object st y in F₁() holds
(F₃() | F₁()) . y = (F₄() | F₁()) . y

proof

let y be object ; :: thesis: ( y in F₁() implies (F₃() | F₁()) . y = (F₄() | F₁()) . y )
assume A17: y in F₁() ; :: thesis: (F₃() | F₁()) . y = (F₄() | F₁()) . y
then reconsider Y = y as Ordinal ;
thus (F₃() | F₁()) . y = F₃() . Y by A17, FUNCT_1:49
.= F₄() . Y by A17, A15
.= (F₄() | F₁()) . y by A17, FUNCT_1:49 ; :: thesis: verum

end;

hence F₃() | F₁() = F₄() | F₁() by A16, FUNCT_1:2; :: thesis: verum