now let x1,
x2,
x3 be
Element of
REAL ;
:: thesis: ( multreal . x1,(addreal . x2,x3) = addreal . (multreal . x1,x2),(multreal . x1,x3) & multreal . (addreal . x1,x2),x3 = addreal . (multreal . x1,x3),(multreal . x2,x3) )thus multreal . x1,
(addreal . x2,x3) =
multreal . x1,
(x2 + x3)
by BINOP_2:def 9
.=
x1 * (x2 + x3)
by BINOP_2:def 11
.=
(x1 * x2) + (x1 * x3)
.=
addreal . (x1 * x2),
(x1 * x3)
by BINOP_2:def 9
.=
addreal . (multreal . x1,x2),
(x1 * x3)
by BINOP_2:def 11
.=
addreal . (multreal . x1,x2),
(multreal . x1,x3)
by BINOP_2:def 11
;
:: thesis: multreal . (addreal . x1,x2),x3 = addreal . (multreal . x1,x3),(multreal . x2,x3)thus multreal . (addreal . x1,x2),
x3 =
multreal . (x1 + x2),
x3
by BINOP_2:def 9
.=
(x1 + x2) * x3
by BINOP_2:def 11
.=
(x1 * x3) + (x2 * x3)
.=
addreal . (x1 * x3),
(x2 * x3)
by BINOP_2:def 9
.=
addreal . (multreal . x1,x3),
(x2 * x3)
by BINOP_2:def 11
.=
addreal . (multreal . x1,x3),
(multreal . x2,x3)
by BINOP_2:def 11
;
:: thesis: verum end;
hence
multreal is_distributive_wrt addreal
by BINOP_1:23; :: thesis: verum