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))) )

hence
the multF of F is_distributive_wrt the addF of F
by BINOP_1:11; :: thesis: verum( 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;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