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

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