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