let K be non empty distributive doubleLoopStr ; :: thesis: the multF of K is_distributive_wrt the addF of K

now :: thesis: 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; :: thesis: ( 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))) ; :: thesis: 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))) ; :: thesis: verum

end;

hence the multF of K is_distributive_wrt the addF of K by BINOP_1:11; :: thesis: verum