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

for a, b, c, p being Element of S st not a _|_ & b _|_ & c _|_ holds

ProJ ((a + p),b,c) = ProJ (a,b,c)

let S be OrtSp of F; :: thesis: for a, b, c, p being Element of S st not a _|_ & b _|_ & c _|_ holds

ProJ ((a + p),b,c) = ProJ (a,b,c)

let a, b, c, p be Element of S; :: thesis: ( not a _|_ & b _|_ & c _|_ implies ProJ ((a + p),b,c) = ProJ (a,b,c) )

assume that

A1: not a _|_ and

A2: b _|_ and

A3: c _|_ ; :: thesis: ProJ ((a + p),b,c) = ProJ (a,b,c)

p _|_ by A2, Th2;

then p _|_ by Def1;

then A4: p _|_ by Th6;

p _|_ by A3, Th2;

then p _|_ by A4, Def1;

then A5: c - ((ProJ (a,b,c)) * b) _|_ by Th2;

a _|_ by A1, Th11;

then c - ((ProJ (a,b,c)) * b) _|_ by Th2;

then c - ((ProJ (a,b,c)) * b) _|_ by A5, Def1;

then A6: a + p _|_ by Th2;

not b _|_ by A1, Th2;

then not b _|_ by A2, Th4;

then A7: not a + p _|_ by Th2;

then a + p _|_ by Th11;

hence ProJ ((a + p),b,c) = ProJ (a,b,c) by A7, A6, Th8; :: thesis: verum

for a, b, c, p being Element of S st not a _|_ & b _|_ & c _|_ holds

ProJ ((a + p),b,c) = ProJ (a,b,c)

let S be OrtSp of F; :: thesis: for a, b, c, p being Element of S st not a _|_ & b _|_ & c _|_ holds

ProJ ((a + p),b,c) = ProJ (a,b,c)

let a, b, c, p be Element of S; :: thesis: ( not a _|_ & b _|_ & c _|_ implies ProJ ((a + p),b,c) = ProJ (a,b,c) )

assume that

A1: not a _|_ and

A2: b _|_ and

A3: c _|_ ; :: thesis: ProJ ((a + p),b,c) = ProJ (a,b,c)

p _|_ by A2, Th2;

then p _|_ by Def1;

then A4: p _|_ by Th6;

p _|_ by A3, Th2;

then p _|_ by A4, Def1;

then A5: c - ((ProJ (a,b,c)) * b) _|_ by Th2;

a _|_ by A1, Th11;

then c - ((ProJ (a,b,c)) * b) _|_ by Th2;

then c - ((ProJ (a,b,c)) * b) _|_ by A5, Def1;

then A6: a + p _|_ by Th2;

not b _|_ by A1, Th2;

then not b _|_ by A2, Th4;

then A7: not a + p _|_ by Th2;

then a + p _|_ by Th11;

hence ProJ ((a + p),b,c) = ProJ (a,b,c) by A7, A6, Th8; :: thesis: verum