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

proof

let B be Ordinal; :: thesis: ( S₁[B] implies S₁[ succ B] )
assume A4: B c= exp C,B ; :: thesis: S₁[ succ B]
( exp C,B <> {} & exp C,(succ B) = C *^ (exp C,B) & exp C,B = 1 *^ (exp C,B) ) by A1, Th22, ORDINAL2:56, ORDINAL2:61;
then exp C,B in exp C,(succ B) by A1, ORDINAL2:57;
then B in exp C,(succ B) by A4, ORDINAL1:22;
hence S₁[ succ B] by ORDINAL1:33; :: thesis: verum

end;

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

proof

let A be Ordinal; :: thesis: ( A <> {} & A is limit_ordinal & ( for B being Ordinal st B in A holds
S₁[B] ) implies S₁[A] )
assume that
A6: ( A <> {} & A is limit_ordinal ) and
A7: for B being Ordinal st B in A holds
B c= exp C,B ; :: thesis: S₁[A]
deffunc H₁( Ordinal) -> set = exp C,$1;
consider fi being Ordinal-Sequence such that
A8: ( dom fi = A & ( for B being Ordinal st B in A holds
fi . B = H₁(B) ) ) from ORDINAL2:sch 3();
fi is increasing by A1, A8, Th25;
then A9: sup fi = lim fi by A6, A8, Th8
.= exp C,A by A6, A8, ORDINAL2:62 ;
let x be set ; :: 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 A8, A10;
then ( exp C,B in rng fi & sup fi = sup (rng fi) ) by A8, A10, FUNCT_1:def 5;
then ( B c= exp C,B & exp C,B in sup fi ) by A7, A10, ORDINAL2:27;
hence x in exp C,A by A9, ORDINAL1:22; :: thesis: verum

end;

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