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

now

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 18
.= 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 18
.= 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:23; :: thesis: verum