let A, C 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:44;
hence S₁[ succ A] by A1, A3, ORDINAL3:31; :: thesis: verum

end;

A4: 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

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
A5: A <> 0 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:45;
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 10;
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 9;
fi . B = exp (C,B) by A8, A9, A14;
hence contradiction by A7, A8, A14, A15; :: thesis: verum

end;

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