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

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