A3: now :: thesis: for A being Ordinal holds not S1[A]
defpred S1[ Ordinal] means not \$1 c= F1(\$1);
assume A4: ex A being Ordinal st S1[A] ; :: thesis: contradiction
consider A being Ordinal such that
A5: S1[A] and
A6: for B being Ordinal st S1[B] holds
A c= B from F1(F1(A)) in F1(A) by ;
then not F1(A) c= F1(F1(A)) by ORDINAL1:5;
hence contradiction by A5, A6; :: thesis: verum
end;
deffunc H1( Ordinal, Sequence) -> set = {} ;
deffunc H2( Ordinal, Ordinal) -> Ordinal = F1(\$2);
consider phi being Ordinal-Sequence such that
A7: dom phi = omega and
A8: ( 0 in omega implies phi . 0 = F1(0) ) and
A9: for A being Ordinal st succ A in omega holds
phi . (succ A) = H2(A,phi . A) and
for A being Ordinal st A in omega & A <> 0 & A is limit_ordinal holds
phi . A = H1(A,phi | A) from assume A10: for A being Ordinal holds not F1(A) = A ; :: thesis: contradiction
A11: now :: thesis: for A being Ordinal holds A in F1(A)
let A be Ordinal; :: thesis: A in F1(A)
A12: A <> F1(A) by A10;
A c= F1(A) by A3;
then A c< F1(A) by A12;
hence A in F1(A) by ORDINAL1:11; :: thesis: verum
end;
A13: phi is increasing
proof
let A be Ordinal; :: according to ORDINAL2:def 12 :: thesis: for b1 being set holds
( not A in b1 or not b1 in dom phi or phi . A in phi . b1 )

let B be Ordinal; :: thesis: ( not A in B or not B in dom phi or phi . A in phi . B )
assume that
A14: A in B and
A15: B in dom phi ; :: thesis: phi . A in phi . B
defpred S1[ Ordinal] means ( A +^ \$1 in omega & \$1 <> {} implies phi . A in phi . (A +^ \$1) );
A16: for B being Ordinal st B <> 0 & B is limit_ordinal & ( for C being Ordinal st C in B holds
S1[C] ) holds
S1[B]
proof
let B be Ordinal; :: thesis: ( B <> 0 & B is limit_ordinal & ( for C being Ordinal st C in B holds
S1[C] ) implies S1[B] )

assume that
A17: B <> 0 and
A18: B is limit_ordinal and
for C being Ordinal st C in B & A +^ C in omega & C <> {} holds
phi . A in phi . (A +^ C) and
A19: A +^ B in omega and
A20: B <> {} ; :: thesis: phi . A in phi . (A +^ B)
A +^ B <> {} by ;
then A21: {} in A +^ B by ORDINAL3:8;
A +^ B is limit_ordinal by ;
then omega c= A +^ B by ;
hence phi . A in phi . (A +^ B) by ; :: thesis: verum
end;
A22: for C being Ordinal st S1[C] holds
S1[ succ C]
proof
let C be Ordinal; :: thesis: ( S1[C] implies S1[ succ C] )
assume that
A23: ( A +^ C in omega & C <> {} implies phi . A in phi . (A +^ C) ) and
A24: A +^ (succ C) in omega and
succ C <> {} ; :: thesis: phi . A in phi . (A +^ (succ C))
reconsider D = phi . (A +^ C) as Ordinal ;
A25: A +^ C in succ (A +^ C) by ORDINAL1:6;
A26: D in F1(D) by A11;
A27: A +^ (succ C) = succ (A +^ C) by ORDINAL2:28;
then phi . (A +^ (succ C)) = F1(D) by ;
hence phi . A in phi . (A +^ (succ C)) by ; :: thesis: verum
end;
A28: S1[ 0 ] ;
A29: for C being Ordinal holds S1[C] from ex C being Ordinal st
( B = A +^ C & C <> {} ) by ;
hence phi . A in phi . B by A7, A15, A29; :: thesis: verum
end;
deffunc H3( Ordinal) -> Ordinal = F1(\$1);
consider fi being Ordinal-Sequence such that
A30: ( dom fi = sup phi & ( for A being Ordinal st A in sup phi holds
fi . A = H3(A) ) ) from H3( {} ) in rng phi by ;
then A31: sup phi <> {} by ORDINAL2:19;
then A32: H3( sup phi) is_limes_of fi by A2, A7, A13, A30, Lm2, Th16;
A33: sup fi c= sup phi
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in sup fi or x in sup phi )
assume A34: x in sup fi ; :: thesis: x in sup phi
then reconsider A = x as Ordinal ;
consider B being Ordinal such that
A35: B in rng fi and
A36: A c= B by ;
consider y being object such that
A37: y in dom fi and
A38: B = fi . y by ;
reconsider y = y as Ordinal by A37;
consider C being Ordinal such that
A39: C in rng phi and
A40: y c= C by ;
( y c< C iff ( y <> C & y c= C ) ) ;
then A41: ( H3(y) in H3(C) or y = C ) by ;
B = H3(y) by ;
then A42: B c= H3(C) by ;
consider z being object such that
A43: z in dom phi and
A44: C = phi . z by ;
reconsider z = z as Ordinal by A43;
A45: succ z in omega by ;
then A46: phi . (succ z) in rng phi by ;
phi . (succ z) = H3(C) by A9, A44, A45;
then H3(C) in sup phi by ;
then B in sup phi by ;
hence x in sup phi by ; :: thesis: verum
end;
A47: fi is increasing
proof
let A be Ordinal; :: according to ORDINAL2:def 12 :: thesis: for b1 being set holds
( not A in b1 or not b1 in dom fi or fi . A in fi . b1 )

let B be Ordinal; :: thesis: ( not A in B or not B in dom fi or fi . A in fi . B )
assume that
A48: A in B and
A49: B in dom fi ; :: thesis: fi . A in fi . B
A50: fi . B = H3(B) by ;
fi . A = H3(A) by ;
hence fi . A in fi . B by A1, A48, A50; :: thesis: verum
end;
sup phi is limit_ordinal by A7, A13, Lm2, Th16;
then sup fi = lim fi by A30, A31, A47, Th8
.= H3( sup phi) by ;
hence contradiction by A11, A33, ORDINAL1:5; :: thesis: verum