let K be non empty distributive doubleLoopStr ; the multF of K is_distributive_wrt the addF of K
now for a1, a2, a3 being Element of K holds
( the multF of K . (a1,( the addF of K . (a2,a3))) = the addF of K . (( the multF of K . (a1,a2)),( the multF of K . (a1,a3))) & the multF of K . (( the addF of K . (a1,a2)),a3) = the addF of K . (( the multF of K . (a1,a3)),( the multF of K . (a2,a3))) )let a1,
a2,
a3 be
Element of
K;
( the multF of K . (a1,( the addF of K . (a2,a3))) = the addF of K . (( the multF of K . (a1,a2)),( the multF of K . (a1,a3))) & the multF of K . (( the addF of K . (a1,a2)),a3) = the addF of K . (( the multF of K . (a1,a3)),( the multF of K . (a2,a3))) )thus the
multF of
K . (
a1,
( the addF of K . (a2,a3))) =
a1 * (a2 + a3)
.=
(a1 * a2) + (a1 * a3)
by VECTSP_1:def 7
.=
the
addF of
K . (
( the multF of K . (a1,a2)),
( the multF of K . (a1,a3)))
;
the multF of K . (( the addF of K . (a1,a2)),a3) = the addF of K . (( the multF of K . (a1,a3)),( the multF of K . (a2,a3)))thus the
multF of
K . (
( the addF of K . (a1,a2)),
a3) =
(a1 + a2) * a3
.=
(a1 * a3) + (a2 * a3)
by VECTSP_1:def 7
.=
the
addF of
K . (
( the multF of K . (a1,a3)),
( the multF of K . (a2,a3)))
;
verum end;
hence
the multF of K is_distributive_wrt the addF of K
by BINOP_1:11; verum