let F be Field; :: thesis: for S being SymSp of F
for b, a, c being Element of S st not a _|_ & a _|_ holds
ProJ (a,b,c) = 1_ F
let S be SymSp of F; :: thesis: for b, a, c being Element of S st not a _|_ & a _|_ holds
ProJ (a,b,c) = 1_ F
let b, a, 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, Th27, VECTSP_1:def 17;
hence ProJ (a,b,c) = 1_ F by A1, Th24; :: thesis: verum