let F be Field; :: thesis: for a, b, c being Element 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 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 13
.= (a * b) - (a * c) by REALSET2:11
.= the addF of F . (((omf F) . (a,b)),((comp F) . (a * c))) by VECTSP_1:def 13
.= (osf F) . (((omf F) . (a,b)),((omf F) . (a,c))) by Def1 ; :: thesis: verum