let C be Ordinal; :: thesis: for A being Ordinal st A <> {} & A is limit_ordinal holds
ex fi being Ordinal-Sequence st
( dom fi = A & ( for B being Ordinal st B in A holds
fi . B = exp C,B ) & ex D being Ordinal st D is_limes_of fi )
defpred S₁[ Ordinal] means ( $1 <> {} & $1 is limit_ordinal & ( for fi being Ordinal-Sequence st dom fi = $1 & ( for B being Ordinal st B in $1 holds
fi . B = exp C,B ) holds
for D being Ordinal holds not D is_limes_of fi ) );
let A be Ordinal; :: thesis: ( A <> {} & A is limit_ordinal implies ex fi being Ordinal-Sequence st
( dom fi = A & ( for B being Ordinal st B in A holds
fi . B = exp C,B ) & ex D being Ordinal st D is_limes_of fi ) )
assume A1: ( A <> {} & A is limit_ordinal & ( for fi being Ordinal-Sequence st dom fi = A & ( for B being Ordinal st B in A holds
fi . B = exp C,B ) holds
for D being Ordinal holds not D is_limes_of fi ) ) ; :: thesis: contradiction
A2: ex A being Ordinal st S₁[A] by A1;
consider A being Ordinal such that
A3: S₁[A] and
A4: for A1 being Ordinal st S₁[A1] holds
A c= A1 from ORDINAL1:sch 1(A2);
deffunc H₁( Ordinal) -> set = exp C,$1;
consider fi being Ordinal-Sequence such that
A5: ( dom fi = A & ( for B being Ordinal st B in A holds
fi . B = H₁(B) ) ) from ORDINAL2:sch 3();

A6: now

assume ( C = {} or C = 1 ) ; :: thesis: contradiction
then ( {} is_limes_of fi or 1 is_limes_of fi ) by A3, A5, Lm6, Lm7;
hence contradiction by A3, A5; :: thesis: verum

end;

then {} in C by ORDINAL3:10;
then 1 c= C by Lm3, ORDINAL1:33;
then A7: 1 c< C by A6, XBOOLE_0:def 8;
then A8: 1 in C by ORDINAL1:21;
A9: for B2, B1 being Ordinal st B1 in B2 & B2 in A holds
exp C,B1 in exp C,B2

proof

defpred S₂[ Ordinal] means for B1 being Ordinal st B1 in $1 & $1 in A holds
exp C,B1 in exp C,$1;
A10: S₂[ {} ] ;
A11: for B being Ordinal st S₂[B] holds
S₂[ succ B]

proof

let B be Ordinal; :: thesis: ( S₂[B] implies S₂[ succ B] )
assume A12: for B1 being Ordinal st B1 in B & B in A holds
exp C,B1 in exp C,B ; :: thesis: S₂[ succ B]
let B1 be Ordinal; :: thesis: ( B1 in succ B & succ B in A implies exp C,B1 in exp C,(succ B) )
assume A13: ( B1 in succ B & succ B in A ) ; :: thesis: exp C,B1 in exp C,(succ B)
A14: exp C,B <> {}

proof

now

per cases ( B = {} or B <> {} ) ;

suppose B = {} ; :: thesis: exp C,B <> {}

hence exp C,B <> {} by ORDINAL2:60; :: thesis: verum

end;

suppose A15: B <> {} ; :: thesis: exp C,B <> {}

B in succ B by ORDINAL1:10;
then B in A by A13, ORDINAL1:19;
hence exp C,B <> {} by A12, A15, ORDINAL3:10; :: thesis: verum

end;

end;

end;

hence exp C,B <> {} ; :: thesis: verum

end;

A16: ( exp C,(succ B) = C *^ (exp C,B) & 1 *^ (exp C,B) = exp C,B & B in succ B ) by ORDINAL1:10, ORDINAL2:56, ORDINAL2:61;
then A17: ( exp C,B in exp C,(succ B) & B in A & B1 c= B ) by A8, A13, A14, ORDINAL1:19, ORDINAL1:34, ORDINAL2:57;

now

assume B1 <> B ; :: thesis: exp C,B1 in exp C,(succ B)
then B1 c< B by A17, XBOOLE_0:def 8;
then B1 in B by ORDINAL1:21;
then exp C,B1 in exp C,B by A12, A17;
hence exp C,B1 in exp C,(succ B) by A17, ORDINAL1:19; :: thesis: verum

end;

hence exp C,B1 in exp C,(succ B) by A7, A14, A16, ORDINAL1:21, ORDINAL2:57; :: thesis: verum

end;

A18: for B being Ordinal st B <> {} & B is limit_ordinal & ( for D being Ordinal st D in B holds
S₂[D] ) holds
S₂[B]

proof

let B be Ordinal; :: thesis: ( B <> {} & B is limit_ordinal & ( for D being Ordinal st D in B holds
S₂[D] ) implies S₂[B] )
assume that
A19: ( B <> {} & B is limit_ordinal ) and
A20: for D being Ordinal st D in B holds
S₂[D] ; :: thesis: S₂[B]
let B1 be Ordinal; :: thesis: ( B1 in B & B in A implies exp C,B1 in exp C,B )
assume A21: ( B1 in B & B in A ) ; :: thesis: exp C,B1 in exp C,B
then consider psi being Ordinal-Sequence such that
A22: ( dom psi = B & ( for D being Ordinal st D in B holds
psi . D = exp C,D ) & ex D being Ordinal st D is_limes_of psi ) by A4, A19, ORDINAL1:7;
A23: exp C,B = lim psi by A19, A22, ORDINAL2:62;
psi is increasing

proof

let B1, B2 be Ordinal; :: according to ORDINAL2:def 16 :: thesis: ( not B1 in B2 or not B2 in dom psi or psi . B1 in psi . B2 )
assume A24: ( B1 in B2 & B2 in dom psi ) ; :: thesis: psi . B1 in psi . B2
then ( S₂[B2] & B2 in A & B1 in B ) by A20, A21, A22, ORDINAL1:19;
then ( exp C,B1 in exp C,B2 & psi . B1 = exp C,B1 & psi . B2 = exp C,B2 ) by A22, A24;
hence psi . B1 in psi . B2 ; :: thesis: verum

end;

then A25: lim psi = sup psi by A19, A22, Th8;
psi . B1 = exp C,B1 by A21, A22;
then ( exp C,B1 in rng psi & sup psi = sup (rng psi) ) by A21, A22, FUNCT_1:def 5;
hence exp C,B1 in exp C,B by A23, A25, ORDINAL2:27; :: thesis: verum

end;

thus for B being Ordinal holds S₂[B] from ORDINAL2:sch 1(A10, A11, A18); :: thesis: verum

end;

fi is increasing

proof

let B1, B2 be Ordinal; :: according to ORDINAL2:def 16 :: thesis: ( not B1 in B2 or not B2 in dom fi or fi . B1 in fi . B2 )
assume A26: ( B1 in B2 & B2 in dom fi ) ; :: thesis: fi . B1 in fi . B2
then B1 in dom fi by ORDINAL1:19;
then ( exp C,B1 in exp C,B2 & fi . B1 = exp C,B1 & fi . B2 = exp C,B2 ) by A5, A9, A26;
hence fi . B1 in fi . B2 ; :: thesis: verum

end;

then sup fi is_limes_of fi by A3, A5, Th8;
hence contradiction by A3, A5; :: thesis: verum