let F be Field; for S being SymSp of F
for b, a, c being Element of S st not a _|_ & c + a _|_ holds
ProJ a,b,c = ProJ c,b,a
let S be SymSp of F; for b, a, c being Element of S st not a _|_ & c + a _|_ holds
ProJ a,b,c = ProJ c,b,a
let b, a, c be Element of S; ( not a _|_ & c + a _|_ implies ProJ a,b,c = ProJ c,b,a )
assume that
A1:
not a _|_
and
A2:
c + a _|_
; ProJ a,b,c = ProJ c,b,a
c + a _|_
by A2, Def1;
then A3:
c + a _|_
by Th16;
a _|_
by A1, Th27;
then
(- ((ProJ a,b,c) * b)) + c _|_
by Th12;
then
a + (- ((ProJ a,b,c) * b)) _|_
by A3, Def1;
then A4:
c _|_
by Th12;
( not b _|_ & b _|_ )
by A1, A2, Th12;
then
not b _|_
by Th13;
then A5:
not c _|_
by Th12;
then
c _|_
by Th27;
hence
ProJ a,b,c = ProJ c,b,a
by A5, A4, Th24; verum