let F be Field; :: thesis: for S being OrtSp of F
for a, b, c being Element of S st not a _|_ & c + a _|_ holds
ProJ (a,b,c) = - (ProJ (c,b,a))

let S be OrtSp of F; :: thesis: for a, b, c being Element of S st not a _|_ & c + a _|_ holds
ProJ (a,b,c) = - (ProJ (c,b,a))

let a, b, c be Element of S; :: thesis: ( not a _|_ & c + a _|_ implies ProJ (a,b,c) = - (ProJ (c,b,a)) )
set 1F = 1_ F;
assume that
A1: not a _|_ and
A2: c + a _|_ ; :: thesis: ProJ (a,b,c) = - (ProJ (c,b,a))
a _|_ by ;
then a _|_ by VECTSP_1:21;
then a _|_ by Def1;
then a _|_ by VECTSP_1:def 14;
then a _|_ by VECTSP_1:def 16;
then a _|_ by VECTSP_1:10;
then a _|_ ;
then a _|_ by VECTSP_1:14;
then ((ProJ (a,b,c)) * b) - c _|_ by Th2;
then A3: ((ProJ (a,b,c)) * b) - c _|_ by Th6;
c + a _|_ by ;
then c - (- a) _|_ by RLVECT_1:17;
then (- a) - ((ProJ (a,b,c)) * b) _|_ by ;
then A4: c _|_ by Th2;
( not b _|_ & b _|_ ) by A1, A2, Th2;
then A5: not b _|_ by Th3;
then A6: not c _|_ by Th2;
then c _|_ by Th11;
then ProJ (a,b,c) = ProJ (c,b,(- a)) by A6, A4, Th8
.= ProJ (c,b,((- (1_ F)) * a)) by VECTSP_1:14
.= (- (1_ F)) * (ProJ (c,b,a)) by
.= - ((ProJ (c,b,a)) * (1_ F)) by VECTSP_1:9 ;
hence ProJ (a,b,c) = - (ProJ (c,b,a)) ; :: thesis: verum