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