let F be Field; 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; 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; ( 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 _|_
; 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; verum