let x, y, z be Element of REAL+ ; :: thesis: x *' (y + z) = (x *' y) + (x *' z)

per cases ( x = {} or y = {} or z = {} or ( x <> {} & y <> {} & z <> {} ) ) ;

suppose A1: x = {} ; :: thesis: x *' (y + z) = (x *' y) + (x *' z)

hence x *' (y + z) = x by Th4
.= x + x by A1, Def8
.= x + (x *' z) by A1, Th4
.= (x *' y) + (x *' z) by A1, Th4 ;
:: thesis: verum

end;

suppose A2: y = {} ; :: thesis: x *' (y + z) = (x *' y) + (x *' z)

hence x *' (y + z) = x *' z by Def8
.= y + (x *' z) by A2, Def8
.= (x *' y) + (x *' z) by A2, Th4 ;
:: thesis: verum

end;

suppose A3: z = {} ; :: thesis: x *' (y + z) = (x *' y) + (x *' z)

hence x *' (y + z) = x *' y by Def8
.= (x *' y) + z by A3, Def8
.= (x *' y) + (x *' z) by A3, Th4 ;
:: thesis: verum

end;

suppose that A4: x <> {} and
A5: ( y <> {} & z <> {} ) ; :: thesis: x *' (y + z) = (x *' y) + (x *' z)

A6: ( x *' y <> {} & x *' z <> {} ) by A4, A5, Lm40;
thus x *' (y + z) = GLUED ((DEDEKIND_CUT x) *' (DEDEKIND_CUT (GLUED ((DEDEKIND_CUT y) + (DEDEKIND_CUT z))))) by A5, Def8
.= GLUED ((DEDEKIND_CUT x) *' ((DEDEKIND_CUT y) + (DEDEKIND_CUT z))) by Lm12
.= GLUED (((DEDEKIND_CUT x) *' (DEDEKIND_CUT y)) + ((DEDEKIND_CUT x) *' (DEDEKIND_CUT z))) by Lm41
.= GLUED (((DEDEKIND_CUT x) *' (DEDEKIND_CUT y)) + (DEDEKIND_CUT (x *' z))) by Lm12
.= GLUED ((DEDEKIND_CUT (x *' y)) + (DEDEKIND_CUT (x *' z))) by Lm12
.= (x *' y) + (x *' z) by A6, Def8 ; :: thesis: verum

end;

end;