let C, A be Ordinal; :: thesis: ( C <> {} implies exp C,A <> {} )
defpred S₁[ Ordinal] means exp C,$1 <> {} ;
assume A1: C <> {} ; :: thesis: exp C,A <> {}
A2: S₁[ {} ] by ORDINAL2:60;
A3: for A being Ordinal st S₁[A] holds
S₁[ succ A]

proof

let A be Ordinal; :: thesis: ( S₁[A] implies S₁[ succ A] )
assume A4: exp C,A <> {} ; :: thesis: S₁[ succ A]
exp C,(succ A) = C *^ (exp C,A) by ORDINAL2:61;
hence S₁[ succ A] by A1, A4, ORDINAL3:34; :: 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
exp C,B <> {} ; :: thesis: S₁[A]
consider fi being Ordinal-Sequence such that
A8: ( 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 ) by A6, Lm8;
A9: exp C,A = lim fi by A6, A8, ORDINAL2:62;
consider D being Ordinal such that
A10: D is_limes_of fi by A8;
A11: lim fi = D by A10, ORDINAL2:def 14;
assume exp C,A = {} ; :: thesis: contradiction
then consider B being Ordinal such that
A12: ( B in dom fi & ( for D being Ordinal st B c= D & D in dom fi holds
fi . D = {} ) ) by A9, A10, A11, ORDINAL2:def 13;
( fi . B = exp C,B & exp C,B <> {} & fi . B = {} ) by A7, A8, A12;
hence contradiction ; :: thesis: verum

end;

for A being Ordinal holds S₁[A] from ORDINAL2:sch 1(A2, A3, A5);
hence exp C,A <> {} ; :: thesis: verum