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

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

S_{1}[ succ B]

S_{1}[D] ) holds

S_{1}[B]

then A26: S_{1}[ 0 ]
by A1, ORDINAL2:35;

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

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

defpred S

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

A2: for B being Ordinal st S

S

proof

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

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

S

S

proof

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

consider fi being Ordinal-Sequence such that

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

fi . D = H_{1}(D) ) )
from ORDINAL2:sch 3();

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

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

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

hence S_{1}[B]
by A25, A10, ORDINAL2:46; :: 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

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

consider fi being Ordinal-Sequence such that

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

fi . D = H

deffunc H

consider f1 being Ordinal-Sequence such that

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

f1 . D = H

deffunc H

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

A10: now :: thesis: ( A <> {} implies S_{1}[B] )

A25:
B *^ {} = {}
by ORDINAL2:38;assume A11:
A <> {}
; :: thesis: S_{1}[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

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_{1}[B]
by A4, A5, A7, ORDINAL2:45; :: thesis: verum

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

A16:
sup (rng f1) = dom f2
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;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

proof

A20:
dom (f2 * f1) = B
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;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

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

now :: thesis: for x being object st x in B holds

fi . x = (f2 * f1) . x

then
fi = f2 * f1
by A7, A20, FUNCT_1:2;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;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

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

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

hence S

then A26: S

for B being Ordinal holds S

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