let A, C be Ordinal; :: thesis: ( 1 in C implies A c= exp (C,A) )
defpred S₁[ Ordinal] means $1 c= exp (C,$1);
assume A1: 1 in C ; :: thesis: A c= exp (C,A)
A2: for B being Ordinal st S₁[B] holds
S₁[ succ B]

proof

let B be Ordinal; :: thesis: ( S₁[B] implies S₁[ succ B] )
assume A3: B c= exp (C,B) ; :: thesis: S₁[ succ B]
A4: exp (C,B) = 1 *^ (exp (C,B)) by ORDINAL2:39;
exp (C,(succ B)) = C *^ (exp (C,B)) by ORDINAL2:44;
then exp (C,B) in exp (C,(succ B)) by A1, A4, Th22, ORDINAL2:40;
then B in exp (C,(succ B)) by A3, ORDINAL1:12;
hence S₁[ succ B] by ORDINAL1:21; :: thesis: verum

end;

A5: for A being Ordinal st A <> 0 & A is limit_ordinal & ( for B being Ordinal st B in A holds
S₁[B] ) holds
S₁[A]

proof

deffunc H₁( Ordinal) -> set = exp (C,$1);
let A be Ordinal; :: thesis: ( A <> 0 & A is limit_ordinal & ( for B being Ordinal st B in A holds
S₁[B] ) implies S₁[A] )
assume that
A6: A <> 0 and
A7: A is limit_ordinal and
A8: for B being Ordinal st B in A holds
B c= exp (C,B) ; :: thesis: S₁[A]
consider fi being Ordinal-Sequence such that
A9: ( dom fi = A & ( for B being Ordinal st B in A holds
fi . B = H₁(B) ) ) from ORDINAL2:sch 3();
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in exp (C,A) )
assume A10: x in A ; :: thesis: x in exp (C,A)
then reconsider B = x as Ordinal ;
fi . B = exp (C,B) by A9, A10;
then exp (C,B) in rng fi by A9, A10, FUNCT_1:def 3;
then A11: exp (C,B) in sup fi by ORDINAL2:19;
fi is increasing by A1, A9, Th25;
then A12: sup fi = lim fi by A6, A7, A9, Th8
.= exp (C,A) by A6, A7, A9, ORDINAL2:45 ;
B c= exp (C,B) by A8, A10;
hence x in exp (C,A) by A12, A11, ORDINAL1:12; :: thesis: verum

end;

A13: S₁[ 0 ] by XBOOLE_1:2;
for B being Ordinal holds S₁[B] from ORDINAL2:sch 1(A13, A2, A5);
hence A c= exp (C,A) ; :: thesis: verum