let A, C be Ordinal; ( 1 in C implies exp (C,A) in exp (C,(succ A)) )
A1:
1 *^ (exp (C,A)) = exp (C,A)
by ORDINAL2:39;
assume
1 in C
; exp (C,A) in exp (C,(succ A))
then
exp (C,A) in C *^ (exp (C,A))
by A1, Th22, ORDINAL2:40;
hence
exp (C,A) in exp (C,(succ A))
by ORDINAL2:44; verum