let F be Field; :: thesis: for S being OrtSp of F

for a, b, c being Element of S st not a _|_ & a _|_ holds

ProJ (a,b,c) = 1_ F

let S be OrtSp of F; :: thesis: for a, b, c being Element of S st not a _|_ & a _|_ holds

ProJ (a,b,c) = 1_ F

let a, b, c be Element of S; :: thesis: ( not a _|_ & a _|_ implies ProJ (a,b,c) = 1_ F )

assume that

A1: not a _|_ and

A2: a _|_ ; :: thesis: ProJ (a,b,c) = 1_ F

( a _|_ & a _|_ ) by A1, A2, Th11, VECTSP_1:def 17;

hence ProJ (a,b,c) = 1_ F by A1, Th8; :: thesis: verum

for a, b, c being Element of S st not a _|_ & a _|_ holds

ProJ (a,b,c) = 1_ F

let S be OrtSp of F; :: thesis: for a, b, c being Element of S st not a _|_ & a _|_ holds

ProJ (a,b,c) = 1_ F

let a, b, c be Element of S; :: thesis: ( not a _|_ & a _|_ implies ProJ (a,b,c) = 1_ F )

assume that

A1: not a _|_ and

A2: a _|_ ; :: thesis: ProJ (a,b,c) = 1_ F

( a _|_ & a _|_ ) by A1, A2, Th11, VECTSP_1:def 17;

hence ProJ (a,b,c) = 1_ F by A1, Th8; :: thesis: verum