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)

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

hence
Lin ((U \ {u}) \/ {(u + (a * v))}) is Subspace of Lin U
by VECTSP_9:16; :: thesis: verum
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)

end;assume A2: x in (U \ {u}) \/ {(u + (a * v))} ; :: thesis: x in the carrier of (Lin U)