let K be Field; :: thesis: for V being VectSp of K
for U being finite Subset of V
for u, v being Vector of V
for a being Element of K st u in U & v in U holds
Lin ((U \ {u}) \/ {(u + (a * v))}) is Subspace of Lin U
let V be VectSp of K; :: thesis: for U being finite Subset of V
for u, v being Vector of V
for a being Element of K st u in U & v in U holds
Lin ((U \ {u}) \/ {(u + (a * v))}) is Subspace of Lin U
let U be finite Subset of V; :: thesis: for u, v being Vector of V
for a being Element of K st u in U & v in U holds
Lin ((U \ {u}) \/ {(u + (a * v))}) is Subspace of Lin U
let u, v be Vector of V; :: thesis: for a being Element of K st u in U & v in U holds
Lin ((U \ {u}) \/ {(u + (a * v))}) is Subspace of Lin U
let a be Element of K; :: thesis: ( u in U & v in U implies Lin ((U \ {u}) \/ {(u + (a * v))}) is Subspace of Lin U )
assume A1: ( u in U & v in U ) ; :: thesis: Lin ((U \ {u}) \/ {(u + (a * v))}) is Subspace of Lin U
set ua = u + (a * v);
set UU = U \ {u};
(U \ {u}) \/ {(u + (a * v))} c= the carrier of (Lin U)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (U \ {u}) \/ {(u + (a * v))} or x in the carrier of (Lin U) )
assume A2: x in (U \ {u}) \/ {(u + (a * v))} ; :: thesis: x in the carrier of (Lin U)

per cases ( x in U \ {u} or x in {(u + (a * v))} ) by A2, XBOOLE_0:def 3;

suppose x in U \ {u} ; :: thesis: x in the carrier of (Lin U)

then x in U by XBOOLE_0:def 5;
then x in Lin U by VECTSP_7:8;
hence x in the carrier of (Lin U) by STRUCT_0:def 5; :: thesis: verum

end;

suppose A3: x in {(u + (a * v))} ; :: thesis: x in the carrier of (Lin U)

A4: ( u in Lin U & a * v in Lin U ) by A1, VECTSP_4:21, VECTSP_7:8;
x = u + (a * v) by A3, TARSKI:def 1;
then x in Lin U by A4, VECTSP_4:20;
hence x in the carrier of (Lin U) by STRUCT_0:def 5; :: thesis: verum

end;

end;

end;

hence Lin ((U \ {u}) \/ {(u + (a * v))}) is Subspace of Lin U by VECTSP_9:16; :: thesis: verum