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

for a, b being Element of S st not a _|_ holds

ProJ (a,b,b) = 1_ F

let S be OrtSp of F; :: thesis: for a, b being Element of S st not a _|_ holds

ProJ (a,b,b) = 1_ F

let a, b be Element of S; :: thesis: ( not a _|_ implies ProJ (a,b,b) = 1_ F )

A1: b - b = 0. S by RLVECT_1:5;

assume not a _|_ ; :: thesis: ProJ (a,b,b) = 1_ F

hence ProJ (a,b,b) = 1_ F by A1, Th1, Th18; :: thesis: verum

for a, b being Element of S st not a _|_ holds

ProJ (a,b,b) = 1_ F

let S be OrtSp of F; :: thesis: for a, b being Element of S st not a _|_ holds

ProJ (a,b,b) = 1_ F

let a, b be Element of S; :: thesis: ( not a _|_ implies ProJ (a,b,b) = 1_ F )

A1: b - b = 0. S by RLVECT_1:5;

assume not a _|_ ; :: thesis: ProJ (a,b,b) = 1_ F

hence ProJ (a,b,b) = 1_ F by A1, Th1, Th18; :: thesis: verum