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);
( exp (exp C,A),{} = 1 & exp C,{} = 1 ) by ORDINAL2:60;
then A1: S₁[ {} ] by ORDINAL2:52;
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

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

now

assume A10: A <> {} ; :: thesis: S₁[B]
A11: dom (f2 * f1) = B

proof

thus dom (f2 * f1) c= B by A7, 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 A12: x in B ; :: thesis: x in dom (f2 * f1)
then reconsider E = x as Ordinal ;
( E *^ A in B *^ A & f1 . E = E *^ A ) by A7, A10, A12, ORDINAL2:57;
hence x in dom (f2 * f1) by A7, A8, A12, FUNCT_1:21; :: thesis: verum

end;

now

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

end;

then A15: fi = f2 * f1 by A6, A11, FUNCT_1:9;
( B *^ A <> {} & B *^ A is limit_ordinal ) by A4, A10, ORDINAL3:34, ORDINAL3:48;
then A16: exp C,(B *^ A) is_limes_of f2 by A8, Th21;
A17: 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
A18: ( y in dom f1 & x = f1 . y ) by FUNCT_1:def 5;
reconsider y = y as Ordinal by A18;
( x = y *^ A & y *^ A in B *^ A ) by A7, A10, A18, ORDINAL2:57;
hence x in dom f2 by A8; :: thesis: verum

end;

A19: sup (rng f1) = dom f2

proof

sup (rng f1) c= sup (dom f2) by A17, 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 A20: x in dom f2 ; :: thesis: x in sup (rng f1)
then reconsider D = x as Ordinal ;
consider A1 being Ordinal such that
A21: ( A1 in B & D in A1 *^ A ) by A4, A8, A20, ORDINAL3:49;
f1 . A1 = A1 *^ A by A7, A21;
then A1 *^ A in rng f1 by A7, A21, FUNCT_1:def 5;
then A1 *^ A in sup (rng f1) by ORDINAL2:27;
hence x in sup (rng f1) by A21, ORDINAL1:19; :: thesis: verum

end;

exp C,(B *^ A) is_limes_of fi by A15, A16, A19, Th14, A7, A10, Th19;
then exp C,(B *^ A) = lim fi by ORDINAL2:def 14;
hence S₁[B] by A4, A6, ORDINAL2:62; :: thesis: verum

end;

hence S₁[B] by A9, ORDINAL2:63; :: thesis: verum

end;

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