let F be Field; for S being OrtSp of F
for a, b, x being Element of S st not a _|_ holds
( a _|_ iff ProJ (a,b,x) = 0. F )
let S be OrtSp of F; for a, b, x being Element of S st not a _|_ holds
( a _|_ iff ProJ (a,b,x) = 0. F )
let a, b, x be Element of S; ( not a _|_ implies ( a _|_ iff ProJ (a,b,x) = 0. F ) )
set 0F = 0. F;
set 0V = 0. S;
hence
( not a _|_ implies ( a _|_ iff ProJ (a,b,x) = 0. F ) )
by A1; verum