let A, B, C be Ordinal; :: thesis: ( 1 in C & A in B implies exp (C,A) in exp (C,B) )
defpred S₁[ 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
S₁[D] ) holds
S₁[B]

proof

deffunc H₁( 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
S₁[D] ) implies S₁[B] )
assume that
A2: B <> 0 and
A3: B is limit_ordinal and
A4: for D being Ordinal st D in B holds
S₁[D] ; :: thesis: S₁[B]
consider fi being Ordinal-Sequence such that
A5: ( dom fi = B & ( for D being Ordinal st D in B holds
fi . D = H₁(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 S₁[B] holds
S₁[ succ B]

proof

let B be Ordinal; :: thesis: ( S₁[B] implies S₁[ succ B] )
assume A14: for A being Ordinal st A in B holds
exp (C,A) in exp (C,B) ; :: thesis: S₁[ 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: S₁[ 0 ] ;
for B being Ordinal holds S₁[B] from ORDINAL2:sch 1(A17, A13, A1);
hence ( not A in B or exp (C,A) in exp (C,B) ) ; :: thesis: verum