let F be Field; :: thesis: for S being OrtSp of F

for a, b, c, p 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; :: thesis: for a, b, c, p 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 a, b, c, p be Element of S; :: thesis: ( 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 _|_ ; :: thesis: ( ProJ (a,(b + p),c) = ProJ (a,b,c) & ProJ (a,b,(c + p)) = ProJ (a,b,c) )

not a _|_ by A1, A2, Th4;

then a _|_ by Th11;

then a _|_ by VECTSP_1:def 14;

then A3: a _|_ by VECTSP_1:17;

( a _|_ & a _|_ ) by A1, A2, Th6, Th11;

then a _|_ by Def1;

then a _|_ by RLVECT_1:def 3;

then a _|_ by RLVECT_1:def 3;

then a _|_ by RLVECT_1:5;

then A4: a _|_ by RLVECT_1:4;

a _|_ by A2, Def1;

then a _|_ by A3, Def1;

then a _|_ by RLVECT_1:def 3;

then a _|_ by RLVECT_1:5;

then A5: a _|_ by RLVECT_1:4;

a _|_ by A1, Th11;

hence ( ProJ (a,(b + p),c) = ProJ (a,b,c) & ProJ (a,b,(c + p)) = ProJ (a,b,c) ) by A1, A5, A4, Th8; :: thesis: verum

for a, b, c, p 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; :: thesis: for a, b, c, p 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 a, b, c, p be Element of S; :: thesis: ( 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 _|_ ; :: thesis: ( ProJ (a,(b + p),c) = ProJ (a,b,c) & ProJ (a,b,(c + p)) = ProJ (a,b,c) )

not a _|_ by A1, A2, Th4;

then a _|_ by Th11;

then a _|_ by VECTSP_1:def 14;

then A3: a _|_ by VECTSP_1:17;

( a _|_ & a _|_ ) by A1, A2, Th6, Th11;

then a _|_ by Def1;

then a _|_ by RLVECT_1:def 3;

then a _|_ by RLVECT_1:def 3;

then a _|_ by RLVECT_1:5;

then A4: a _|_ by RLVECT_1:4;

a _|_ by A2, Def1;

then a _|_ by A3, Def1;

then a _|_ by RLVECT_1:def 3;

then a _|_ by RLVECT_1:5;

then A5: a _|_ by RLVECT_1:4;

a _|_ by A1, Th11;

hence ( ProJ (a,(b + p),c) = ProJ (a,b,c) & ProJ (a,b,(c + p)) = ProJ (a,b,c) ) by A1, A5, A4, Th8; :: thesis: verum