let A, C be Ordinal; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum

A1: 1 *^ (exp (C,A)) = exp (C,A) by ORDINAL2:39;

assume 1 in C ; :: thesis: 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; :: thesis: verum