let F be Field; :: thesis: for S being OrtSp of F
for a, b, c being Element of S st not a _|_ & not a _|_ holds
ProJ (a,b,c) = (ProJ (a,c,b)) "
let S be OrtSp of F; :: thesis: for a, b, c being Element of S st not a _|_ & not a _|_ holds
ProJ (a,b,c) = (ProJ (a,c,b)) "
let a, b, 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, Th20;
(ProJ (a,b,b)) * ((ProJ (a,b,c)) ") = ProJ (a,c,b) by A1, A2, Th21;
then ((ProJ (a,b,c)) ") * (1_ F) = ProJ (a,c,b) by A1, Th19;
then A4: (ProJ (a,b,c)) " = ProJ (a,c,b) ;
ProJ (a,b,c) <> 0. F by A1, A2, Th20;
then 1_ F = (ProJ (a,c,b)) * (ProJ (a,b,c)) by A4, VECTSP_1:def 10;
then (ProJ (a,c,b)) " = ((ProJ (a,c,b)) ") * ((ProJ (a,c,b)) * (ProJ (a,b,c)))
.= (((ProJ (a,c,b)) ") * (ProJ (a,c,b))) * (ProJ (a,b,c)) by GROUP_1:def 3
.= (ProJ (a,b,c)) * (1_ F) by A3, VECTSP_1:def 10 ;
hence ProJ (a,b,c) = (ProJ (a,c,b)) " ; :: thesis: verum