let F be Field; the multF of F is_distributive_wrt the addF of F
now 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 18
.=
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 18
.=
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:23; verum