let F be Field; :: thesis: for a, b, c being Element of the carrier of F holds (omf F) . a,((osf F) . b,c) = (osf F) . ((omf F) . a,b),((omf F) . a,c)
let a, b, c be Element of the carrier of F; :: thesis: (omf F) . a,((osf F) . b,c) = (osf F) . ((omf F) . a,b),((omf F) . a,c)
thus (omf F) . a,((osf F) . b,c) = (omf F) . a,(the addF of F . b,((comp F) . c)) by Def1
.= a * (b - c) by VECTSP_1:def 25
.= (a * b) - (a * c) by REALSET2:15
.= the addF of F . ((omf F) . a,b),((comp F) . (a * c)) by VECTSP_1:def 25
.= (osf F) . ((omf F) . a,b),((omf F) . a,c) by Def1 ; :: thesis: verum