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_{1}[ 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_{1}( Ordinal) -> set = exp (C,$1);

A4: ex A being Ordinal st S_{1}[A]
by A1, A2, A3;

consider A being Ordinal such that

A5: S_{1}[A]
and

A6: for A1 being Ordinal st S_{1}[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_{1}(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)

hence contradiction by A5, A7; :: thesis: verum

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

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

A4: ex A being Ordinal st S

consider A being Ordinal such that

A5: S

A6: for A1 being Ordinal st S

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

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

fi is increasing
defpred S_{2}[ 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_{2}[B] holds

S_{2}[ succ B]

S_{2}[D] ) holds

S_{2}[B]
_{2}[ 0 ]
;

thus for B being Ordinal holds S_{2}[B]
from ORDINAL2:sch 1(A35, A11, A22); :: thesis: verum

end;exp (C,B1) in exp (C,$1);

A11: for B being Ordinal st S

S

proof

A22:
for B being Ordinal st B <> 0 & B is limit_ordinal & ( for D being Ordinal st D in B holds
let B be Ordinal; :: thesis: ( S_{2}[B] implies S_{2}[ 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_{2}[ 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) <> {}

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

end;assume A12: for B1 being Ordinal st B1 in B & B in A holds

exp (C,B1) in exp (C,B) ; :: thesis: S

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

end;

A20:
exp (C,(succ B)) = C *^ (exp (C,B))
by ORDINAL2:44;now :: thesis: exp (C,B) <> {}

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

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)) )

hence
exp (C,B1) in exp (C,(succ B))
by A9, A18, A20, A17, ORDINAL1:11, ORDINAL2:40; :: thesis: verumassume
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;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

S

S

proof

A35:
S
let B be Ordinal; :: thesis: ( B <> 0 & B is limit_ordinal & ( for D being Ordinal st D in B holds

S_{2}[D] ) implies S_{2}[B] )

assume that

A23: B <> 0 and

A24: B is limit_ordinal and

A25: for D being Ordinal st D in B holds

S_{2}[D]
; :: thesis: S_{2}[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

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;S

assume that

A23: B <> 0 and

A24: B is limit_ordinal and

A25: for D being Ordinal st D in B holds

S

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

then A34:
lim psi = sup psi
by A23, A24, A28, Th8;
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;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

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

thus for B being Ordinal holds S

proof

then
sup fi is_limes_of fi
by A5, A7, Th8;
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;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

hence contradiction by A5, A7; :: thesis: verum