let F be Field; for S being OrtSp of F
for a, b being Element of S st a _|_ & b _|_ holds
a - b _|_
let S be OrtSp of F; for a, b being Element of S st a _|_ & b _|_ holds
a - b _|_
let a, b be Element of S; ( a _|_ & b _|_ implies a - b _|_ )
set 0V = 0. S;
assume that
A1:
a _|_
and
A2:
b _|_
; a - b _|_
a _|_
by A1, Def1;
then
a _|_
by VECTSP_1:14;
then
- a _|_
by Th2;
then
(0. S) + (- a) _|_
by RLVECT_1:4;
then
(b + (- b)) + (- a) _|_
by RLVECT_1:5;
then
b + ((- b) - a) _|_
by RLVECT_1:def 3;
then A3:
b - (a + b) _|_
by VECTSP_1:17;
b + (0. S) _|_
by A2, RLVECT_1:4;
then
b + (a + (- a)) _|_
by RLVECT_1:5;
then
(a + b) - a _|_
by RLVECT_1:def 3;
hence
a - b _|_
by A3, Def1; verum