let A, B, C be Ordinal; :: thesis: exp (C,(A +^ B)) = (exp (C,B)) *^ (exp (C,A))

defpred S_{1}[ 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_{1}[B] holds

S_{1}[ succ B]

S_{1}[D] ) holds

S_{1}[B]

then A18: S_{1}[ 0 ]
by A1, ORDINAL2:27;

for B being Ordinal holds S_{1}[B]
from ORDINAL2:sch 1(A18, A2, A4);

hence exp (C,(A +^ B)) = (exp (C,B)) *^ (exp (C,A)) ; :: thesis: verum

defpred S

A1: 1 = exp (C,{}) by ORDINAL2:43;

A2: for B being Ordinal st S

S

proof

A4:
for B being Ordinal st B <> 0 & B is limit_ordinal & ( for D being Ordinal st D in B holds
let B be Ordinal; :: thesis: ( S_{1}[B] implies S_{1}[ succ B] )

assume A3: exp (C,(A +^ B)) = (exp (C,B)) *^ (exp (C,A)) ; :: thesis: S_{1}[ 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;assume A3: exp (C,(A +^ B)) = (exp (C,B)) *^ (exp (C,A)) ; :: thesis: S

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

S

S

proof

exp (C,A) = 1 *^ (exp (C,A))
by ORDINAL2:39;
deffunc H_{1}( 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_{1}[D] ) implies S_{1}[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_{1}[B]

consider fi being Ordinal-Sequence such that

A8: ( dom fi = B & ( for D being Ordinal st D in B holds

fi . D = H_{1}(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_{1}(D) ) )
from ORDINAL2:sch 3();

deffunc H_{2}( 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_{2}(D) ) )
from ORDINAL2:sch 3();

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_{1}[B]
by A16, ORDINAL2:def 10; :: thesis: verum

end;let B be Ordinal; :: thesis: ( B <> 0 & B is limit_ordinal & ( for D being Ordinal st D in B holds

S

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

consider fi being Ordinal-Sequence such that

A8: ( dom fi = B & ( for D being Ordinal st D in B holds

fi . D = H

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

deffunc H

consider f1 being Ordinal-Sequence such that

A10: ( dom f1 = A & ( for D being Ordinal st D in A holds

f1 . D = H

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

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;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

A13: now :: thesis: for D being Ordinal st D in dom f1 holds

psi . D = f1 . D

dom psi = (dom f1) +^ (dom (fi *^ (exp (C,A))))
by A8, A9, A10, ORDINAL3:def 4;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;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

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

then A18: S

for B being Ordinal holds S

hence exp (C,(A +^ B)) = (exp (C,B)) *^ (exp (C,A)) ; :: thesis: verum