now :: thesis: for x1, x2, x3 being Element of REAL holds
( multreal . (x1,(addreal . (x2,x3))) = addreal . ((multreal . (x1,x2)),(multreal . (x1,x3))) & multreal . ((addreal . (x1,x2)),x3) = addreal . ((multreal . (x1,x3)),(multreal . (x2,x3))) )

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:11; :: thesis: verum