let A, B, C be Ordinal; :: thesis: exp (C,(A +^ B)) = (exp (C,B)) *^ (exp (C,A))
defpred S₁[ 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 S₁[B] holds
S₁[ succ B]

proof

let B be Ordinal; :: thesis: ( S₁[B] implies S₁[ succ B] )
assume A3: exp (C,(A +^ B)) = (exp (C,B)) *^ (exp (C,A)) ; :: thesis: S₁[ 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 A3, ORDINAL3:50
.= (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
S₁[D] ) holds
S₁[B]

proof

deffunc H₁( 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
S₁[D] ) implies S₁[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: S₁[B]
consider fi being Ordinal-Sequence such that
A8: ( dom fi = B & ( for D being Ordinal st D in B holds
fi . D = H₁(D) ) ) from ORDINAL2:sch 3();
consider psi being Ordinal-Sequence such that
A9: ( dom psi = A +^ B & ( for D being Ordinal st D in A +^ B holds
psi . D = H₁(D) ) ) from ORDINAL2:sch 3();
deffunc H₂( 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 = H₂(D) ) ) from ORDINAL2:sch 3();

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 A8, A9, A10, ORDINAL2:32
.= (exp (C,D)) *^ (exp (C,A)) by A7, A8, A12
.= (fi . D) *^ (exp (C,A)) by A8, A12
.= (fi *^ (exp (C,A))) . D by A12, ORDINAL3:def 4 ;
:: 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 A10, A14 ;
:: thesis: verum

end;

dom psi = (dom f1) +^ (dom (fi *^ (exp (C,A)))) by A8, A9, A10, ORDINAL3:def 4;
then A15: psi = f1 ^ (fi *^ (exp (C,A))) by A13, A11, Def1;
(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 A15, Th3;
A17: A +^ B <> {} by A5, ORDINAL3:26;
A +^ B is limit_ordinal by A5, A6, ORDINAL3:29;
then lim psi = exp (C,(A +^ B)) by A9, A17, ORDINAL2:45;
hence S₁[B] by A16, ORDINAL2:def 10; :: thesis: verum

end;

exp (C,A) = 1 *^ (exp (C,A)) by ORDINAL2:39;
then A18: S₁[ 0 ] by A1, ORDINAL2:27;
for B being Ordinal holds S₁[B] from ORDINAL2:sch 1(A18, A2, A4);
hence exp (C,(A +^ B)) = (exp (C,B)) *^ (exp (C,A)) ; :: thesis: verum