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: for A being Ordinal st S₁[A] holds
S₁[ succ A]

proof

let A be Ordinal; :: thesis: ( S₁[A] implies S₁[ succ A] )
assume A3: exp C,A <> {} ; :: thesis: S₁[ succ A]
exp C,(succ A) = C *^ (exp C,A) by ORDINAL2:61;
hence S₁[ succ A] by A1, A3, ORDINAL3:34; :: thesis: verum

end;

A4: 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
A5: A <> {} and
A6: 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 and
A9: for B being Ordinal st B in A holds
fi . B = exp C,B and
A10: ex D being Ordinal st D is_limes_of fi by A5, A6, Lm8;
A11: exp C,A = lim fi by A5, A6, A8, A9, ORDINAL2:62;
assume A12: exp C,A = {} ; :: thesis: contradiction
consider D being Ordinal such that
A13: D is_limes_of fi by A10;
lim fi = D by A13, ORDINAL2:def 14;
then consider B being Ordinal such that
A14: B in dom fi and
A15: for D being Ordinal st B c= D & D in dom fi holds
fi . D = {} by A11, A13, A12, ORDINAL2:def 13;
fi . B = exp C,B by A8, A9, A14;
hence contradiction by A7, A8, A14, A15; :: thesis: verum

end;

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