let F be Field; :: thesis: for S being OrtSp of F
for b, a, x, y being Element of st not a _|_ & x = 0. S holds
PProJ a,b,x,y = 0. F
let S be OrtSp of F; :: thesis: for b, a, x, y being Element of st not a _|_ & x = 0. S holds
PProJ a,b,x,y = 0. F
let b, a, x, y be Element of ; :: 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 holds
( a _|_ or x _|_ ) by A2, Th11, Th12;
hence PProJ a,b,x,y = 0. F by A1, Def7; :: thesis: verum