let K be Field; :: thesis: for V being VectSp of K
for W being Subspace of V
for v being Vector of V
for w being Vector of W st v = w holds
Lin {w} = Lin {v}
let V be VectSp of K; :: thesis: for W being Subspace of V
for v being Vector of V
for w being Vector of W st v = w holds
Lin {w} = Lin {v}
let W be Subspace of V; :: thesis: for v being Vector of V
for w being Vector of W st v = w holds
Lin {w} = Lin {v}
let v be Vector of V; :: thesis: for w being Vector of W st v = w holds
Lin {w} = Lin {v}
let w be Vector of W; :: thesis: ( v = w implies Lin {w} = Lin {v} )
assume A1: v = w ; :: thesis: Lin {w} = Lin {v}
reconsider W1 = Lin {w} as Subspace of V by VECTSP_4:26;
now :: thesis: for u being Vector of V holds
( ( u in W1 implies u in Lin {v} ) & ( u in Lin {v} implies u in W1 ) )
let u be Vector of V; :: thesis: ( ( u in W1 implies u in Lin {v} ) & ( u in Lin {v} implies u in W1 ) )
hereby :: thesis: ( u in Lin {v} implies u in W1 )
assume u in W1 ; :: thesis: u in Lin {v}
then consider a being Element of K such that
A2: u = a * w by Th3;
u = a * v by A1, A2, VECTSP_4:14;
hence u in Lin {v} by Th3; :: thesis: verum
end;
assume u in Lin {v} ; :: thesis: u in W1
then consider a being Element of K such that
A3: u = a * v by Th3;
u = a * w by A1, A3, VECTSP_4:14;
hence u in W1 by Th3; :: thesis: verum
end;
hence Lin {w} = Lin {v} by VECTSP_4:30; :: thesis: verum