let F be Field; :: thesis: for S being SymSp of F
for b, a, c being Element of S st not a _|_ & not a _|_ holds
ProJ a,b,c = (ProJ a,c,b) "
let S be SymSp of F; :: thesis: for b, a, c being Element of S st not a _|_ & not a _|_ holds
ProJ a,b,c = (ProJ a,c,b) "
let b, a, c be Element of S; :: thesis: ( not a _|_ & not a _|_ implies ProJ a,b,c = (ProJ a,c,b) " )
set 1F = 1_ F;
set 0F = 0. F;
assume that
A1: not a _|_ and
A2: not a _|_ ; :: thesis: ProJ a,b,c = (ProJ a,c,b) "
A3: ProJ a,c,b <> 0. F by A1, A2, Th36;
(ProJ a,b,b) * ((ProJ a,b,c) " ) = ProJ a,c,b by A1, A2, Th37;
then ((ProJ a,b,c) " ) * (1_ F) = ProJ a,c,b by A1, Th35;
then A4: (ProJ a,b,c) " = ProJ a,c,b by VECTSP_1:def 19;
ProJ a,b,c <> 0. F by A1, A2, Th36;
then 1_ F = (ProJ a,c,b) * (ProJ a,b,c) by A4, VECTSP_1:def 22;
then (ProJ a,c,b) " = ((ProJ a,c,b) " ) * ((ProJ a,c,b) * (ProJ a,b,c)) by VECTSP_1:def 19
.= (((ProJ a,c,b) " ) * (ProJ a,c,b)) * (ProJ a,b,c) by GROUP_1:def 4
.= (ProJ a,b,c) * (1_ F) by A3, VECTSP_1:def 22 ;
hence ProJ a,b,c = (ProJ a,c,b) " by VECTSP_1:def 19; :: thesis: verum