let F be Field; :: thesis: the multF of F is_distributive_wrt the addF of F
now :: thesis: 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; :: thesis: ( 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))) ; :: thesis: 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))) ; :: thesis: verum
end;
hence the multF of F is_distributive_wrt the addF of F by BINOP_1:11; :: thesis: verum