let F be Field; :: thesis: for S being SymSp of F
for b, a, q, p 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 SymSp of F; :: thesis: for b, a, q, p being Element of S st not a _|_ & not a _|_ holds
(ProJ a,b,p) * ((ProJ a,b,q) " ) = ProJ a,q,p
let b, a, q, p 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, Th27;
then a _|_ by Def1;
then a _|_ by RLVECT_1:def 6;
then a _|_ by RLVECT_1:def 6;
then a _|_ by RLVECT_1:16;
then a _|_ by RLVECT_1:10;
then A3: a _|_ by A1, Th28;
a _|_ by A1, Th27;
then (ProJ a,q,p) * (ProJ a,b,q) = ProJ a,b,p by A1, A3, Th24;
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 4;
ProJ a,b,q <> 0. F by A1, A2, Th36;
then (ProJ a,q,p) * (1_ F) = (ProJ a,b,p) * ((ProJ a,b,q) " ) by A4, VECTSP_1:def 22;
hence (ProJ a,b,p) * ((ProJ a,b,q) " ) = ProJ a,q,p by VECTSP_1:def 19; :: thesis: verum