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 25
.= - (b - a) by RLVECT_1:47
.= (comp F) . (b + (- a)) by VECTSP_1:def 25
.= (comp F) . (the addF of F . b,((comp F) . a)) by VECTSP_1:def 25 ;
hence (osf F) . a,b = (comp F) . ((osf F) . b,a) by Def1; :: thesis: verum