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: S₁[ {} ]

proof

thus (A +^ {} ) *^ C = A *^ C by ORDINAL2:44
.= (A *^ C) +^ {} by ORDINAL2:44
.= (A *^ C) +^ ({} *^ C) by ORDINAL2:52 ; :: thesis: verum

end;

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 A3: (A +^ B) *^ C = (A *^ C) +^ (B *^ C) ; :: thesis: S₁[ succ B]
thus (A +^ (succ B)) *^ C = (succ (A +^ B)) *^ C by ORDINAL2:45
.= ((A *^ C) +^ (B *^ C)) +^ C by A3, ORDINAL2:53
.= (A *^ C) +^ ((B *^ C) +^ C) by Th33
.= (A *^ C) +^ ((succ B) *^ C) by ORDINAL2:53 ; :: thesis: verum

end;

A4: 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 A5: ( B <> {} & B is limit_ordinal & ( for D being Ordinal st D in B holds
S₁[D] ) ) ; :: thesis: S₁[B]
deffunc H₁( Ordinal) -> set = 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 *^ C;
consider psi being Ordinal-Sequence such that
A7: ( dom psi = B & ( for D being Ordinal st D in B holds
psi . D = H₂(D) ) ) from ORDINAL2:sch 3();
A8: ( A +^ B = sup fi & A +^ B is limit_ordinal ) by A5, A6, Th32, ORDINAL2:46;
A9: ( dom (fi *^ C) = dom fi & dom ((A *^ C) +^ psi) = dom psi ) by Def2, Def5;

now

let x be set ; :: thesis: ( x in B implies (fi *^ C) . x = ((A *^ C) +^ psi) . x )
assume A10: 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 A6, A10, Def5
.= (A +^ k) *^ C by A6, A10
.= (A *^ C) +^ (k *^ C) by A5, A10
.= (A *^ C) +^ n by A7, A10
.= ((A *^ C) +^ psi) . x by A7, A10, Def2 ; :: thesis: verum

end;

then A11: fi *^ C = (A *^ C) +^ psi by A6, A7, A9, FUNCT_1:9;
A12: {} in B by A5, Th10;
reconsider k = psi . {} as Ordinal ;
A13: k in rng psi by A7, A12, FUNCT_1:def 5;
then A14: k in sup (rng psi) by ORDINAL2:27;
A15: ( sup psi <> {} & (A +^ B) *^ C is limit_ordinal ) by A8, A13, Th48, ORDINAL2:27;

A16: now

assume C <> {} ; :: thesis: (A +^ B) *^ C = (A *^ C) +^ (B *^ C)
then (A +^ B) *^ C = sup (fi *^ C) by A5, A6, A8, Th52
.= (A *^ C) +^ (sup psi) by A5, A7, A11, Th51 ;
hence (A +^ B) *^ C = union ((A *^ C) +^ (sup psi)) by A15, ORDINAL1:def 6
.= (A *^ C) +^ (union (sup psi)) by A14, Th53
.= (A *^ C) +^ (B *^ C) by A5, A7, ORDINAL2:54 ;
:: thesis: verum

end;

now

assume C = {} ; :: thesis: S₁[B]
then ( (A +^ B) *^ C = {} & A *^ C = {} & B *^ C = {} & {} +^ {} = {} ) by ORDINAL2:44, ORDINAL2:55;
hence S₁[B] ; :: thesis: verum

end;

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

end;

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