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 ;
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 ;
x = u + (a * v) by ;
then x in Lin U by ;
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