let F be Field; 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; (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; verum