let F be Field; :: thesis: for S being SymSp of F
for b, a being Element of S st not a _|_ holds
ProJ a,b,b = 1_ F
let S be SymSp of F; :: thesis: for b, a being Element of S st not a _|_ holds
ProJ a,b,b = 1_ F
let b, a be Element of S; :: thesis: ( not a _|_ implies ProJ a,b,b = 1_ F )
A1: b - b = 0. S by RLVECT_1:16;
assume not a _|_ ; :: thesis: ProJ a,b,b = 1_ F
hence ProJ a,b,b = 1_ F by A1, Th11, Th34; :: thesis: verum