let F be Field; :: thesis: 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; :: thesis: 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; :: thesis: ( not a _|_ implies ( a _|_ iff ProJ (a,b,x) = 0. F ) )

set 0F = 0. F;

set 0V = 0. S;

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; :: thesis: 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; :: thesis: ( not a _|_ implies ( a _|_ iff ProJ (a,b,x) = 0. F ) )

set 0F = 0. F;

set 0V = 0. S;

A1: now :: thesis: ( not a _|_ & a _|_ implies ProJ (a,b,x) = 0. F )

assume that

A2: not a _|_ and

A3: a _|_ ; :: thesis: ProJ (a,b,x) = 0. F

a _|_ by A3, RLVECT_1:4;

then a _|_ by RLVECT_1:12;

then A4: a _|_ by VECTSP_1:14;

a _|_ by A2, Th11;

hence ProJ (a,b,x) = 0. F by A2, A4, Th8; :: thesis: verum

end;A2: not a _|_ and

A3: a _|_ ; :: thesis: ProJ (a,b,x) = 0. F

a _|_ by A3, RLVECT_1:4;

then a _|_ by RLVECT_1:12;

then A4: a _|_ by VECTSP_1:14;

a _|_ by A2, Th11;

hence ProJ (a,b,x) = 0. F by A2, A4, Th8; :: thesis: verum

now :: thesis: ( not a _|_ & ProJ (a,b,x) = 0. F implies a _|_ )

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

then a _|_ by Th11;

then a _|_ by VECTSP_1:14;

then a _|_ by RLVECT_1:12;

hence a _|_ by RLVECT_1:4; :: thesis: verum

end;then a _|_ by Th11;

then a _|_ by VECTSP_1:14;

then a _|_ by RLVECT_1:12;

hence a _|_ by RLVECT_1:4; :: thesis: verum