let A, B, C be Ordinal; :: thesis: (A +^ B) *^ C = (A *^ C) +^ (B *^ C)
defpred S₁[ Ordinal] means (A +^ $1) *^ C = (A *^ C) +^ ($1 *^ C);
A1: for B being Ordinal st S₁[B] holds
S₁[ succ B]

proof

let B be Ordinal; :: thesis: ( S₁[B] implies S₁[ succ B] )
assume A2: (A +^ B) *^ C = (A *^ C) +^ (B *^ C) ; :: thesis: S₁[ succ B]
thus (A +^ (succ B)) *^ C = (succ (A +^ B)) *^ C by ORDINAL2:28
.= ((A *^ C) +^ (B *^ C)) +^ C by A2, ORDINAL2:36
.= (A *^ C) +^ ((B *^ C) +^ C) by Th30
.= (A *^ C) +^ ((succ B) *^ C) 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 = 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
S₁[D] ; :: 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();
A +^ B is limit_ordinal by A4, A5, Th29;
then A8: (A +^ B) *^ C is limit_ordinal by Th40;
A9: dom (fi *^ C) = dom fi by Def4;

A10: now :: thesis: ( C = {} implies S₁[B] )

assume A11: C = {} ; :: thesis: S₁[B]
then A12: A *^ C = {} by ORDINAL2:38;
A13: B *^ C = {} by A11, ORDINAL2:38;
(A +^ B) *^ C = {} by A11, ORDINAL2:38;
hence S₁[B] by A12, A13, ORDINAL2:27; :: thesis: verum

end;

deffunc H₂( Ordinal) -> set = $1 *^ C;
consider psi being Ordinal-Sequence such that
A14: ( dom psi = B & ( for D being Ordinal st D in B holds
psi . D = H₂(D) ) ) from ORDINAL2:sch 3();

A15: now :: thesis: for x being object st x in B holds
(fi *^ C) . x = ((A *^ C) +^ psi) . x

let x be object ; :: thesis: ( x in B implies (fi *^ C) . x = ((A *^ C) +^ psi) . x )
assume A16: x in B ; :: thesis: (fi *^ C) . x = ((A *^ C) +^ psi) . x
then reconsider k = x as Ordinal ;
reconsider m = fi . k, n = psi . k as Ordinal ;
thus (fi *^ C) . x = m *^ C by A7, A16, Def4
.= (A +^ k) *^ C by A7, A16
.= (A *^ C) +^ (k *^ C) by A6, A16
.= (A *^ C) +^ n by A14, A16
.= ((A *^ C) +^ psi) . x by A14, A16, Def1 ; :: thesis: verum

end;

reconsider k = psi . {} as Ordinal ;
{} in B by A4, Th8;
then k in rng psi by A14, FUNCT_1:def 3;
then A17: k in sup (rng psi) by ORDINAL2:19;
dom ((A *^ C) +^ psi) = dom psi by Def1;
then A18: fi *^ C = (A *^ C) +^ psi by A7, A14, A9, A15, FUNCT_1:2;
A19: A +^ B = sup fi by A4, A5, A7, ORDINAL2:29;

now :: thesis: ( C <> {} implies (A +^ B) *^ C = (A *^ C) +^ (B *^ C) )

assume C <> {} ; :: thesis: (A +^ B) *^ C = (A *^ C) +^ (B *^ C)
then (A +^ B) *^ C = sup (fi *^ C) by A4, A5, A7, A19, Th29, Th44
.= (A *^ C) +^ (sup psi) by A4, A14, A18, Th43 ;
hence (A +^ B) *^ C = union ((A *^ C) +^ (sup psi)) by A8
.= (A *^ C) +^ (union (sup psi)) by A17, Th45
.= (A *^ C) +^ (B *^ C) by A4, A5, A14, ORDINAL2:37 ;
:: thesis: verum

end;

hence S₁[B] by A10; :: thesis: verum

end;

(A +^ {}) *^ C = A *^ C by ORDINAL2:27
.= (A *^ C) +^ {} by ORDINAL2:27
.= (A *^ C) +^ ({} *^ C) by ORDINAL2:35 ;
then A20: S₁[ 0 ] ;
for B being Ordinal holds S₁[B] from ORDINAL2:sch 1(A20, A1, A3);
hence (A +^ B) *^ C = (A *^ C) +^ (B *^ C) ; :: thesis: verum