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

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