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

for a, b, x, y being Element of S st not a _|_ & x = 0. S holds

PProJ (a,b,x,y) = 0. F

let S be OrtSp of F; :: thesis: for a, b, x, y being Element of S st not a _|_ & x = 0. S holds

PProJ (a,b,x,y) = 0. F

let a, b, x, y be Element of S; :: thesis: ( not a _|_ & x = 0. S implies PProJ (a,b,x,y) = 0. F )

assume that

A1: not a _|_ and

A2: x = 0. S ; :: thesis: PProJ (a,b,x,y) = 0. F

for p being Element of S holds

( a _|_ or x _|_ ) by A2, Th1, Th2;

hence PProJ (a,b,x,y) = 0. F by A1, Def3; :: thesis: verum

for a, b, x, y being Element of S st not a _|_ & x = 0. S holds

PProJ (a,b,x,y) = 0. F

let S be OrtSp of F; :: thesis: for a, b, x, y being Element of S st not a _|_ & x = 0. S holds

PProJ (a,b,x,y) = 0. F

let a, b, x, y be Element of S; :: thesis: ( not a _|_ & x = 0. S implies PProJ (a,b,x,y) = 0. F )

assume that

A1: not a _|_ and

A2: x = 0. S ; :: thesis: PProJ (a,b,x,y) = 0. F

for p being Element of S holds

( a _|_ or x _|_ ) by A2, Th1, Th2;

hence PProJ (a,b,x,y) = 0. F by A1, Def3; :: thesis: verum