let C, A, B be Ordinal; :: thesis: exp (exp C,A),B = exp C,(B *^ A)
defpred S₁[ Ordinal] means exp (exp C,A),$1 = exp C,($1 *^ A);
A1: exp C,{} = 1 by ORDINAL2:60;
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 exp (exp C,A),B = exp C,(B *^ A) ; :: thesis: S₁[ succ B]
hence exp (exp C,A),(succ B) = (exp C,A) *^ (exp C,(B *^ A)) by ORDINAL2:61
.= exp C,((B *^ A) +^ A) by Th30
.= exp C,((succ B) *^ A) by ORDINAL2:53 ;
:: thesis: verum

end;

A3: 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

deffunc H₁( Ordinal) -> set = exp (exp C,A),$1;
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
A4: B <> {} and
A5: B is limit_ordinal and
A6: for D being Ordinal st D in B holds
exp (exp C,A),D = exp C,(D *^ A) ; :: thesis: S₁[B]
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();
deffunc H₂( Ordinal) -> set = $1 *^ A;
consider f1 being Ordinal-Sequence such that
A8: ( dom f1 = B & ( for D being Ordinal st D in B holds
f1 . D = H₂(D) ) ) from ORDINAL2:sch 3();
deffunc H₃( Ordinal) -> set = exp C,$1;
consider f2 being Ordinal-Sequence such that
A9: ( dom f2 = B *^ A & ( for D being Ordinal st D in B *^ A holds
f2 . D = H₃(D) ) ) from ORDINAL2:sch 3();

A10: now

assume A11: A <> {} ; :: thesis: S₁[B]
then B *^ A <> {} by A4, ORDINAL3:34;
then A12: exp C,(B *^ A) is_limes_of f2 by A5, A9, Th21, ORDINAL3:48;
A13: rng f1 c= dom f2

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f1 or x in dom f2 )
assume x in rng f1 ; :: thesis: x in dom f2
then consider y being set such that
A14: y in dom f1 and
A15: x = f1 . y by FUNCT_1:def 5;
reconsider y = y as Ordinal by A14;
x = y *^ A by A8, A14, A15;
hence x in dom f2 by A8, A9, A11, A14, ORDINAL2:57; :: thesis: verum

end;

A16: sup (rng f1) = dom f2

proof

sup (rng f1) c= sup (dom f2) by A13, ORDINAL2:30;
hence sup (rng f1) c= dom f2 by ORDINAL2:26; :: according to XBOOLE_0:def 10 :: thesis: dom f2 c= sup (rng f1)
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom f2 or x in sup (rng f1) )
assume A17: x in dom f2 ; :: thesis: x in sup (rng f1)
then reconsider D = x as Ordinal ;
consider A1 being Ordinal such that
A18: A1 in B and
A19: D in A1 *^ A by A5, A9, A17, ORDINAL3:49;
f1 . A1 = A1 *^ A by A8, A18;
then A1 *^ A in rng f1 by A8, A18, FUNCT_1:def 5;
then A1 *^ A in sup (rng f1) by ORDINAL2:27;
hence x in sup (rng f1) by A19, ORDINAL1:19; :: thesis: verum

end;

A20: dom (f2 * f1) = B

proof

thus dom (f2 * f1) c= B by A8, RELAT_1:44; :: according to XBOOLE_0:def 10 :: thesis: B c= dom (f2 * f1)
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in dom (f2 * f1) )
assume A21: x in B ; :: thesis: x in dom (f2 * f1)
then reconsider E = x as Ordinal ;
A22: f1 . E = E *^ A by A8, A21;
E *^ A in B *^ A by A11, A21, ORDINAL2:57;
hence x in dom (f2 * f1) by A8, A9, A21, A22, FUNCT_1:21; :: thesis: verum

end;

now

let x be set ; :: thesis: ( x in B implies fi . x = (f2 * f1) . x )
assume A23: x in B ; :: thesis: fi . x = (f2 * f1) . x
then reconsider D = x as Ordinal ;
A24: f1 . D = D *^ A by A8, A23;
thus fi . x = exp (exp C,A),D by A7, A23
.= exp C,(D *^ A) by A6, A23
.= f2 . (f1 . D) by A9, A11, A23, A24, ORDINAL2:57
.= (f2 * f1) . x by A8, A23, FUNCT_1:23 ; :: thesis: verum

end;

then fi = f2 * f1 by A7, A20, FUNCT_1:9;
then exp C,(B *^ A) is_limes_of fi by A8, A11, A12, A16, Th14, Th19;
then exp C,(B *^ A) = lim fi by ORDINAL2:def 14;
hence S₁[B] by A4, A5, A7, ORDINAL2:62; :: thesis: verum

end;

A25: B *^ {} = {} by ORDINAL2:55;
exp C,{} = 1 by ORDINAL2:60;
hence S₁[B] by A25, A10, ORDINAL2:63; :: thesis: verum

end;

exp (exp C,A),{} = 1 by ORDINAL2:60;
then A26: S₁[ {} ] by A1, ORDINAL2:52;
for B being Ordinal holds S₁[B] from ORDINAL2:sch 1(A26, A2, A3);
hence exp (exp C,A),B = exp C,(B *^ A) ; :: thesis: verum