let A, B, C be Ordinal; :: thesis: ( 1 in C & A in B implies exp (C,A) in exp (C,B) )
defpred S1[ Ordinal] means for A being Ordinal st A in $1 holds
exp (C,A) in exp (C,$1);
A1: for B being Ordinal st B <> 0 & B is limit_ordinal & ( for D being Ordinal st D in B holds
S1[D] ) holds
S1[B]
proof
deffunc H1( Ordinal) -> set = exp (C,$1);
let B be Ordinal; :: thesis: ( B <> 0 & B is limit_ordinal & ( for D being Ordinal st D in B holds
S1[D] ) implies S1[B] )
assume that
A2: B <> 0 and
A3: B is limit_ordinal and
A4: for D being Ordinal st D in B holds
S1[D] ; :: thesis: S1[B]
consider fi being Ordinal-Sequence such that
A5: ( dom fi = B & ( for D being Ordinal st D in B holds
fi . D = H1(D) ) ) from ORDINAL2:sch 3();
 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
A6: B1 in B2 and
A7: B2 in dom fi ; :: thesis: fi . B1 in fi . B2
A8: fi . B1 = exp (C,B1) by A5, A6, A7, ORDINAL1:10;
exp (C,B1) in exp (C,B2) by A4, A5, A6, A7;
hence fi . B1 in fi . B2 by A5, A7, A8; :: thesis: verum
end;
then A9: sup fi = lim fi by A2, A3, A5, Th8;
let A be Ordinal; :: thesis: ( A in B implies exp (C,A) in exp (C,B) )
assume A10: A in B ; :: thesis: exp (C,A) in exp (C,B)
fi . A = exp (C,A) by A10, A5;
then A11: exp (C,A) in rng fi by A10, A5, FUNCT_1:def 3;
exp (C,B) = lim fi by A2, A3, A5, ORDINAL2:45;
hence exp (C,A) in exp (C,B) by A9, A11, ORDINAL2:19; :: thesis: verum
end;
assume A12: 1 in C ; :: thesis: ( not A in B or exp (C,A) in exp (C,B) )
A13: for B being Ordinal st S1[B] holds
S1[ succ B]
proof
let B be Ordinal; :: thesis: ( S1[B] implies S1[ succ B] )
assume A14: for A being Ordinal st A in B holds
exp (C,A) in exp (C,B) ; :: thesis: S1[ succ B]
let A be Ordinal; :: thesis: ( A in succ B implies exp (C,A) in exp (C,(succ B)) )
assume A in succ B ; :: thesis: exp (C,A) in exp (C,(succ B))
then A15: A c= B by ORDINAL1:22;
A16: now :: thesis: ( A <> B implies exp (C,A) in exp (C,B) )
assume A <> B ; :: thesis: exp (C,A) in exp (C,B)
then A c< B by A15;
hence exp (C,A) in exp (C,B) by A14, ORDINAL1:11; :: thesis: verum
end;
exp (C,B) in exp (C,(succ B)) by A12, Th23;
hence exp (C,A) in exp (C,(succ B)) by A16, ORDINAL1:10; :: thesis: verum
end;
A17: S1[ 0 ] ;
for B being Ordinal holds S1[B] from ORDINAL2:sch 1(A17, A13, A1);
 hence ( not A in B or exp (C,A) in exp (C,B) ) ; :: thesis: verum