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