let A, B, C be Ordinal; :: thesis: exp (C,(A +^ B)) = (exp (C,B)) *^ (exp (C,A))
defpred S1[ Ordinal] means exp (C,(A +^ \$1)) = (exp (C,\$1)) *^ (exp (C,A));
A1: 1 = exp (C,{}) by ORDINAL2:43;
A2: for B being Ordinal st S1[B] holds
S1[ succ B]
proof
let B be Ordinal; :: thesis: ( S1[B] implies S1[ succ B] )
assume A3: exp (C,(A +^ B)) = (exp (C,B)) *^ (exp (C,A)) ; :: thesis: S1[ succ B]
thus exp (C,(A +^ (succ B))) = exp (C,(succ (A +^ B))) by ORDINAL2:28
.= C *^ (exp (C,(A +^ B))) by ORDINAL2:44
.= (C *^ (exp (C,B))) *^ (exp (C,A)) by
.= (exp (C,(succ B))) *^ (exp (C,A)) by ORDINAL2:44 ; :: thesis: verum
end;
A4: for B being Ordinal st B <> 0 & B is limit_ordinal & ( for D being Ordinal st D in B holds
S1[D] ) holds
S1[B]
proof
deffunc H1( Ordinal) -> set = exp (C,\$1);
let B be Ordinal; :: thesis: ( B <> 0 & B is limit_ordinal & ( for D being Ordinal st D in B holds
S1[D] ) implies S1[B] )

assume that
A5: B <> 0 and
A6: B is limit_ordinal and
A7: for D being Ordinal st D in B holds
exp (C,(A +^ D)) = (exp (C,D)) *^ (exp (C,A)) ; :: thesis: S1[B]
consider fi being Ordinal-Sequence such that
A8: ( dom fi = B & ( for D being Ordinal st D in B holds
fi . D = H1(D) ) ) from consider psi being Ordinal-Sequence such that
A9: ( dom psi = A +^ B & ( for D being Ordinal st D in A +^ B holds
psi . D = H1(D) ) ) from deffunc H2( Ordinal) -> set = exp (C,\$1);
consider f1 being Ordinal-Sequence such that
A10: ( dom f1 = A & ( for D being Ordinal st D in A holds
f1 . D = H2(D) ) ) from
A11: now :: thesis: for D being Ordinal st D in dom (fi *^ (exp (C,A))) holds
psi . ((dom f1) +^ D) = (fi *^ (exp (C,A))) . D
let D be Ordinal; :: thesis: ( D in dom (fi *^ (exp (C,A))) implies psi . ((dom f1) +^ D) = (fi *^ (exp (C,A))) . D )
assume D in dom (fi *^ (exp (C,A))) ; :: thesis: psi . ((dom f1) +^ D) = (fi *^ (exp (C,A))) . D
then A12: D in dom fi by ORDINAL3:def 4;
hence psi . ((dom f1) +^ D) = exp (C,(A +^ D)) by
.= (exp (C,D)) *^ (exp (C,A)) by A7, A8, A12
.= (fi . D) *^ (exp (C,A)) by
.= (fi *^ (exp (C,A))) . D by ;
:: thesis: verum
end;
A13: now :: thesis: for D being Ordinal st D in dom f1 holds
psi . D = f1 . D
let D be Ordinal; :: thesis: ( D in dom f1 implies psi . D = f1 . D )
assume A14: D in dom f1 ; :: thesis: psi . D = f1 . D
A c= A +^ B by ORDINAL3:24;
hence psi . D = exp (C,D) by A9, A10, A14
.= f1 . D by ;
:: thesis: verum
end;
dom psi = (dom f1) +^ (dom (fi *^ (exp (C,A)))) by ;
then A15: psi = f1 ^ (fi *^ (exp (C,A))) by ;
(exp (C,B)) *^ (exp (C,A)) is_limes_of fi *^ (exp (C,A)) by A5, A6, A8, Th5, Th21;
then A16: (exp (C,B)) *^ (exp (C,A)) is_limes_of psi by ;
A17: A +^ B <> {} by ;
A +^ B is limit_ordinal by ;
then lim psi = exp (C,(A +^ B)) by ;
hence S1[B] by A16, ORDINAL2:def 10; :: thesis: verum
end;
exp (C,A) = 1 *^ (exp (C,A)) by ORDINAL2:39;
then A18: S1[ 0 ] by ;
for B being Ordinal holds S1[B] from hence exp (C,(A +^ B)) = (exp (C,B)) *^ (exp (C,A)) ; :: thesis: verum