let F be Field; :: thesis: for x being Element of F holds (osf F) . (x,x) = 0. F
let x be Element of F; :: thesis: (osf F) . (x,x) = 0. F
thus (osf F) . (x,x) = the addF of F . (x,((comp F) . x)) by Def1
.= x - x by VECTSP_1:def 13
.= 0. F by RLVECT_1:5 ; :: thesis: verum