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

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

(ProJ (a,b,p)) * ((ProJ (a,b,q)) ") = ProJ (a,q,p)

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

(ProJ (a,b,p)) * ((ProJ (a,b,q)) ") = ProJ (a,q,p)

let a, b, p, q be Element of S; :: thesis: ( not a _|_ & not a _|_ implies (ProJ (a,b,p)) * ((ProJ (a,b,q)) ") = ProJ (a,q,p) )

assume that

A1: not a _|_ and

A2: not a _|_ ; :: thesis: (ProJ (a,b,p)) * ((ProJ (a,b,q)) ") = ProJ (a,q,p)

( a _|_ & a _|_ ) by A1, A2, Th11;

then a _|_ by Def1;

then a _|_ by RLVECT_1:def 3;

then a _|_ by RLVECT_1:def 3;

then a _|_ by RLVECT_1:5;

then a _|_ by RLVECT_1:4;

then A3: a _|_ by A1, Th12;

a _|_ by A1, Th11;

then (ProJ (a,q,p)) * (ProJ (a,b,q)) = ProJ (a,b,p) by A1, A3, Th8;

then A4: (ProJ (a,q,p)) * ((ProJ (a,b,q)) * ((ProJ (a,b,q)) ")) = (ProJ (a,b,p)) * ((ProJ (a,b,q)) ") by GROUP_1:def 3;

ProJ (a,b,q) <> 0. F by A1, A2, Th20;

then (ProJ (a,q,p)) * (1_ F) = (ProJ (a,b,p)) * ((ProJ (a,b,q)) ") by A4, VECTSP_1:def 10;

hence (ProJ (a,b,p)) * ((ProJ (a,b,q)) ") = ProJ (a,q,p) ; :: thesis: verum

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

(ProJ (a,b,p)) * ((ProJ (a,b,q)) ") = ProJ (a,q,p)

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

(ProJ (a,b,p)) * ((ProJ (a,b,q)) ") = ProJ (a,q,p)

let a, b, p, q be Element of S; :: thesis: ( not a _|_ & not a _|_ implies (ProJ (a,b,p)) * ((ProJ (a,b,q)) ") = ProJ (a,q,p) )

assume that

A1: not a _|_ and

A2: not a _|_ ; :: thesis: (ProJ (a,b,p)) * ((ProJ (a,b,q)) ") = ProJ (a,q,p)

( a _|_ & a _|_ ) by A1, A2, Th11;

then a _|_ by Def1;

then a _|_ by RLVECT_1:def 3;

then a _|_ by RLVECT_1:def 3;

then a _|_ by RLVECT_1:5;

then a _|_ by RLVECT_1:4;

then A3: a _|_ by A1, Th12;

a _|_ by A1, Th11;

then (ProJ (a,q,p)) * (ProJ (a,b,q)) = ProJ (a,b,p) by A1, A3, Th8;

then A4: (ProJ (a,q,p)) * ((ProJ (a,b,q)) * ((ProJ (a,b,q)) ")) = (ProJ (a,b,p)) * ((ProJ (a,b,q)) ") by GROUP_1:def 3;

ProJ (a,b,q) <> 0. F by A1, A2, Th20;

then (ProJ (a,q,p)) * (1_ F) = (ProJ (a,b,p)) * ((ProJ (a,b,q)) ") by A4, VECTSP_1:def 10;

hence (ProJ (a,b,p)) * ((ProJ (a,b,q)) ") = ProJ (a,q,p) ; :: thesis: verum