let F be Field; :: thesis: for S being SymSp of F
for a, b, x, y being Element of S st (1_ F) + (1_ F) <> 0. F & not a _|_ & x = 0. S holds
PProJ (a,b,x,y) = 0. F
let S be SymSp of F; :: thesis: for a, b, x, y being Element of S st (1_ F) + (1_ F) <> 0. F & not a _|_ & x = 0. S holds
PProJ (a,b,x,y) = 0. F
let a, b, x, y be Element of S; :: thesis: ( (1_ F) + (1_ F) <> 0. F & not a _|_ & x = 0. S implies PProJ (a,b,x,y) = 0. F )
assume that
A1: ( (1_ F) + (1_ F) <> 0. F & 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