let F be Field; :: thesis: for x being Element of the carrier of F holds (osf F) . x,x = 0. F
let x be Element of the carrier 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 25
.= 0. F by RLVECT_1:16 ; :: thesis: verum