let A, B, C 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: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 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:44
.= exp (C,((B *^ A) +^ A)) by Th30
.= exp (C,((succ B) *^ A)) by ORDINAL2:36 ;
:: thesis: verum

end;

A3: 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 ((exp (C,A)),$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
A4: B <> 0 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 :: thesis: ( A <> {} implies S₁[B] )

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

proof

let x be object ; :: 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 object such that
A14: y in dom f1 and
A15: x = f1 . y by FUNCT_1:def 3;
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:40; :: thesis: verum

end;

A16: sup (rng f1) = dom f2

proof

sup (rng f1) c= sup (dom f2) by A13, ORDINAL2:22;
hence sup (rng f1) c= dom f2 by ORDINAL2:18; :: according to XBOOLE_0:def 10 :: thesis: dom f2 c= sup (rng f1)
let x be object ; :: 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:41;
f1 . A1 = A1 *^ A by A8, A18;
then A1 *^ A in rng f1 by A8, A18, FUNCT_1:def 3;
then A1 *^ A in sup (rng f1) by ORDINAL2:19;
hence x in sup (rng f1) by A19, ORDINAL1:10; :: thesis: verum

end;

A20: dom (f2 * f1) = B

proof

thus dom (f2 * f1) c= B by A8, RELAT_1:25; :: according to XBOOLE_0:def 10 :: thesis: B c= dom (f2 * f1)
let x be object ; :: 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:40;
hence x in dom (f2 * f1) by A8, A9, A21, A22, FUNCT_1:11; :: thesis: verum

end;

now :: thesis: for x being object st x in B holds
fi . x = (f2 * f1) . x

let x be object ; :: 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:40
.= (f2 * f1) . x by A8, A23, FUNCT_1:13 ; :: thesis: verum

end;

then fi = f2 * f1 by A7, A20, FUNCT_1:2;
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 10;
hence S₁[B] by A4, A5, A7, ORDINAL2:45; :: thesis: verum

end;

A25: B *^ {} = {} by ORDINAL2:38;
exp (C,{}) = 1 by ORDINAL2:43;
hence S₁[B] by A25, A10, ORDINAL2:46; :: thesis: verum

end;

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