let F be Ring; :: thesis: for V, W 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, W 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})
A2: Lin (A \/ {y}) = (Lin A) + (Lin {y}) by VECTSP_7:15;
y in {y} by TARSKI:def 1;
then A3: y in Lin {y} by VECTSP_7:8;
(x - y) + y = x - (y - y) by RLVECT_1:29
.= x - (0. V) by VECTSP_1:19
.= x by RLVECT_1:13 ;
hence x in Lin (A \/ {y}) by A1, A3, A2, VECTSP_5:1; :: thesis: verum