let C, A, B 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);
( exp C,A = 1 *^ (exp C,A) & 1 = exp C,{} ) by ORDINAL2:56, ORDINAL2:60;
then A1: S₁[ {} ] by ORDINAL2:44;
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:45
.= C *^ (exp C,(A +^ B)) by ORDINAL2:61
.= (C *^ (exp C,B)) *^ (exp C,A) by A3, ORDINAL3:58
.= (exp C,(succ B)) *^ (exp C,A) by ORDINAL2:61 ; :: thesis: verum

end;

A4: for B being Ordinal st B <> {} & B is limit_ordinal & ( for D being Ordinal st D in B holds
S₁[D] ) holds
S₁[B]

proof

let B be Ordinal; :: thesis: ( B <> {} & B is limit_ordinal & ( for D being Ordinal st D in B holds
S₁[D] ) implies S₁[B] )
assume that
A5: ( B <> {} & B is limit_ordinal ) and
A6: for D being Ordinal st D in B holds
exp C,(A +^ D) = (exp C,D) *^ (exp C,A) ; :: thesis: S₁[B]
deffunc H₁( Ordinal) -> set = exp C,$1;
consider fi being Ordinal-Sequence such that
A7: ( 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
A8: ( dom psi = A +^ B & ( for D being Ordinal st D in A +^ B holds
psi . D = H₁(D) ) ) from ORDINAL2:sch 3();
( A +^ B <> {} & A +^ B is limit_ordinal ) by A5, ORDINAL3:29, ORDINAL3:32;
then A9: lim psi = exp C,(A +^ B) by A8, ORDINAL2:62;
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: dom psi = (dom f1) +^ (dom (fi *^ (exp C,A))) by A7, A8, A10, ORDINAL3:def 5;

A12: now

let D be Ordinal; :: thesis: ( D in dom f1 implies psi . D = f1 . D )
assume A13: D in dom f1 ; :: thesis: psi . D = f1 . D
A c= A +^ B by ORDINAL3:27;
hence psi . D = exp C,D by A8, A10, A13
.= f1 . D by A10, A13 ;
:: thesis: verum

end;

A14: exp C,B is_limes_of fi by A5, A7, Th21;

now

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 A15: D in dom fi by ORDINAL3:def 5;
hence psi . ((dom f1) +^ D) = exp C,(A +^ D) by A8, A10, A7, ORDINAL2:49
.= (exp C,D) *^ (exp C,A) by A6, A7, A15
.= (fi . D) *^ (exp C,A) by A7, A15
.= (fi *^ (exp C,A)) . D by A15, ORDINAL3:def 5 ;
:: thesis: verum

end;

then ( psi = f1 ^ (fi *^ (exp C,A)) & (exp C,B) *^ (exp C,A) is_limes_of fi *^ (exp C,A) ) by A11, A12, A14, Def1, Th5;
then (exp C,B) *^ (exp C,A) is_limes_of psi by Th3;
hence S₁[B] by A9, ORDINAL2:def 14; :: thesis: verum

end;

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