let F be Field; :: thesis: for a, b being Element of F holds (osf F) . (a,b) = (comp F) . ((osf F) . (b,a))
let a, b be Element of F; :: thesis: (osf F) . (a,b) = (comp F) . ((osf F) . (b,a))
(osf F) . (a,b) = the addF of F . (a,((comp F) . b)) by Def1
.= a + (- b) by VECTSP_1:def 13
.= - (b - a) by RLVECT_1:33
.= (comp F) . (b + (- a)) by VECTSP_1:def 13
.= (comp F) . ( the addF of F . (b,((comp F) . a))) by VECTSP_1:def 13 ;
hence (osf F) . (a,b) = (comp F) . ((osf F) . (b,a)) by Def1; :: thesis: verum