let F be Field; :: thesis: for V being VectSp of F
for A being Subset of V
for x, y being Element of V st x - y in Lin A holds
x in Lin (A \/ {y})
let V be VectSp of F; :: thesis: for A being Subset of V
for x, y being Element of V st x - y in Lin A holds
x in Lin (A \/ {y})
let A be Subset of V; :: thesis: for x, y being Element of V st x - y in Lin A holds
x in Lin (A \/ {y})
let x, y be Element of V; :: thesis: ( x - y in Lin A implies x in Lin (A \/ {y}) )
assume A1: x - y in Lin A ; :: thesis: x in Lin (A \/ {y})
y in {y} by TARSKI:def 1;
then A2: y in Lin {y} by VECTSP_7:13;
A3: (x - y) + y = x - (y - y) by RLVECT_1:43
.= x - (0. V) by VECTSP_1:66
.= x by RLVECT_1:26 ;
Lin (A \/ {y}) = (Lin A) + (Lin {y}) by VECTSP_7:20;
hence x in Lin (A \/ {y}) by A1, A2, A3, VECTSP_5:5; :: thesis: verum