let F be Field; the multF of F is_distributive_wrt the addF of F
now for x, y, z being Element of F holds
( the multF of F . (x,( the addF of F . (y,z))) = the addF of F . (( the multF of F . (x,y)),( the multF of F . (x,z))) & the multF of F . (( the addF of F . (x,y)),z) = the addF of F . (( the multF of F . (x,z)),( the multF of F . (y,z))) )let x,
y,
z be
Element of
F;
( the multF of F . (x,( the addF of F . (y,z))) = the addF of F . (( the multF of F . (x,y)),( the multF of F . (x,z))) & the multF of F . (( the addF of F . (x,y)),z) = the addF of F . (( the multF of F . (x,z)),( the multF of F . (y,z))) )thus the
multF of
F . (
x,
( the addF of F . (y,z))) =
x * (y + z)
.=
(x * y) + (x * z)
by VECTSP_1:def 7
.=
the
addF of
F . (
( the multF of F . (x,y)),
( the multF of F . (x,z)))
;
the multF of F . (( the addF of F . (x,y)),z) = the addF of F . (( the multF of F . (x,z)),( the multF of F . (y,z)))thus the
multF of
F . (
( the addF of F . (x,y)),
z) =
(x + y) * z
.=
(x * z) + (y * z)
by VECTSP_1:def 7
.=
the
addF of
F . (
( the multF of F . (x,z)),
( the multF of F . (y,z)))
;
verum end;
hence
the multF of F is_distributive_wrt the addF of F
by BINOP_1:11; verum