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 that
A1: A <> {} and
A2: A is limit_ordinal and
A3: 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
deffunc H₁( Ordinal) -> set = exp (C,$1);
A4: ex A being Ordinal st S₁[A] by A1, A2, A3;
consider A being Ordinal such that
A5: S₁[A] and
A6: for A1 being Ordinal st S₁[A1] holds
A c= A1 from ORDINAL1:sch 1(A4);
consider fi being Ordinal-Sequence such that
A7: ( dom fi = A & ( for B being Ordinal st B in A holds
fi . B = H₁(B) ) ) from ORDINAL2:sch 3();
A8: ( C <> {} & C <> 1 ) by A5, A7, Lm6, Lm7;
then {} in C by ORDINAL3:8;
then 1 c= C by Lm3, ORDINAL1:21;
then A9: 1 c< C by A8;
A10: 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);
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 that
A13: B1 in succ B and
A14: succ B in A ; :: thesis: exp (C,B1) in exp (C,(succ B))
A15: B1 c= B by A13, ORDINAL1:22;
B in succ B by ORDINAL1:6;
then A16: B in A by A14, ORDINAL1:10;
A17: 1 *^ (exp (C,B)) = exp (C,B) by ORDINAL2:39;
A18: exp (C,B) <> {}

proof

now :: thesis: exp (C,B) <> {}

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

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

hence exp (C,B) <> {} by ORDINAL2:43; :: thesis: verum

end;

suppose A19: B <> {} ; :: thesis: exp (C,B) <> {}

B in succ B by ORDINAL1:6;
then B in A by A14, ORDINAL1:10;
hence exp (C,B) <> {} by A12, A19, ORDINAL3:8; :: thesis: verum

end;

end;

end;

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

end;

A20: exp (C,(succ B)) = C *^ (exp (C,B)) by ORDINAL2:44;
then A21: exp (C,B) in exp (C,(succ B)) by A9, A18, A17, ORDINAL1:11, ORDINAL2:40;

now :: thesis: ( B1 <> B implies exp (C,B1) in exp (C,(succ B)) )

assume B1 <> B ; :: thesis: exp (C,B1) in exp (C,(succ B))
then B1 c< B by A15;
then B1 in B by ORDINAL1:11;
then exp (C,B1) in exp (C,B) by A12, A16;
hence exp (C,B1) in exp (C,(succ B)) by A21, ORDINAL1:10; :: thesis: verum

end;

hence exp (C,B1) in exp (C,(succ B)) by A9, A18, A20, A17, ORDINAL1:11, ORDINAL2:40; :: thesis: verum

end;

A22: for B being Ordinal st B <> 0 & 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 <> 0 & B is limit_ordinal & ( for D being Ordinal st D in B holds
S₂[D] ) implies S₂[B] )
assume that
A23: B <> 0 and
A24: B is limit_ordinal and
A25: 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 that
A26: B1 in B and
A27: B in A ; :: thesis: exp (C,B1) in exp (C,B)
consider psi being Ordinal-Sequence such that
A28: dom psi = B and
A29: for D being Ordinal st D in B holds
psi . D = exp (C,D) and
ex D being Ordinal st D is_limes_of psi by A6, A24, A26, A27, ORDINAL1:5;
psi . B1 = exp (C,B1) by A26, A29;
then A30: exp (C,B1) in rng psi by A26, A28, FUNCT_1:def 3;
psi is increasing

proof

let B1, B2 be Ordinal; :: according to ORDINAL2:def 12 :: thesis: ( not B1 in B2 or not B2 in dom psi or psi . B1 in psi . B2 )
assume that
A31: B1 in B2 and
A32: B2 in dom psi ; :: thesis: psi . B1 in psi . B2
B2 in A by A27, A28, A32, ORDINAL1:10;
then A33: exp (C,B1) in exp (C,B2) by A25, A28, A31, A32;
psi . B1 = exp (C,B1) by A28, A29, A31, A32, ORDINAL1:10;
hence psi . B1 in psi . B2 by A28, A29, A32, A33; :: thesis: verum

end;

then A34: lim psi = sup psi by A23, A24, A28, Th8;
exp (C,B) = lim psi by A23, A24, A28, A29, ORDINAL2:45;
hence exp (C,B1) in exp (C,B) by A34, A30, ORDINAL2:19; :: thesis: verum

end;

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

end;

fi is increasing

proof

let B1, B2 be Ordinal; :: according to ORDINAL2:def 12 :: thesis: ( not B1 in B2 or not B2 in dom fi or fi . B1 in fi . B2 )
assume that
A36: B1 in B2 and
A37: B2 in dom fi ; :: thesis: fi . B1 in fi . B2
A38: fi . B1 = exp (C,B1) by A7, A36, A37, ORDINAL1:10;
exp (C,B1) in exp (C,B2) by A7, A10, A36, A37;
hence fi . B1 in fi . B2 by A7, A37, A38; :: thesis: verum

end;

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