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

A1: now

assume that
A2: not a _|_ and
A3: a _|_ ; :: thesis: ProJ (a,b,x) = 0. F
a _|_ by A3, RLVECT_1:10;
then a _|_ by RLVECT_1:25;
then A4: a _|_ by VECTSP_1:59;
a _|_ by A2, Th24;
hence ProJ (a,b,x) = 0. F by A2, A4, Th20; :: thesis: verum

end;

now

assume ( not a _|_ & ProJ (a,b,x) = 0. F ) ; :: thesis: a _|_
then a _|_ by Th24;
then a _|_ by VECTSP_1:59;
then a _|_ by RLVECT_1:25;
hence a _|_ by RLVECT_1:10; :: thesis: verum

end;

hence ( not a _|_ implies ( a _|_ iff ProJ (a,b,x) = 0. F ) ) by A1; :: thesis: verum