let F be Field; for S being OrtSp of F
for b, a, p, c being Element of S st not a _|_ & a _|_ holds
( ProJ (a,(b + p),c) = ProJ (a,b,c) & ProJ (a,b,(c + p)) = ProJ (a,b,c) )
let S be OrtSp of F; for b, a, p, c being Element of S st not a _|_ & a _|_ holds
( ProJ (a,(b + p),c) = ProJ (a,b,c) & ProJ (a,b,(c + p)) = ProJ (a,b,c) )
let b, a, p, c be Element of S; ( not a _|_ & a _|_ implies ( ProJ (a,(b + p),c) = ProJ (a,b,c) & ProJ (a,b,(c + p)) = ProJ (a,b,c) ) )
set 0V = 0. S;
assume that
A1:
not a _|_
and
A2:
a _|_
; ( ProJ (a,(b + p),c) = ProJ (a,b,c) & ProJ (a,b,(c + p)) = ProJ (a,b,c) )
not a _|_
by A1, A2, Th14;
then
a _|_
by Th24;
then
a _|_
by VECTSP_1:def 26;
then A3:
a _|_
by VECTSP_1:64;
( a _|_ & a _|_ )
by A1, A2, Th16, Th24;
then
a _|_
by Def2;
then
a _|_
by RLVECT_1:def 6;
then
a _|_
by RLVECT_1:def 6;
then
a _|_
by RLVECT_1:16;
then A4:
a _|_
by RLVECT_1:10;
a _|_
by A2, Def2;
then
a _|_
by A3, Def2;
then
a _|_
by RLVECT_1:def 6;
then
a _|_
by RLVECT_1:16;
then A5:
a _|_
by RLVECT_1:10;
a _|_
by A1, Th24;
hence
( ProJ (a,(b + p),c) = ProJ (a,b,c) & ProJ (a,b,(c + p)) = ProJ (a,b,c) )
by A1, A5, A4, Th20; verum