let V be RealLinearSpace; :: 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 RLSUB_1:27;
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 Real such that
A2: u = a * w by RLVECT_4:8;
u = a * v by A1, A2, RLSUB_1:14;
hence u in Lin {v} by RLVECT_4:8; :: thesis: verum
end;
assume u in Lin {v} ; :: thesis: u in W1
then consider a being Real such that
A3: u = a * v by RLVECT_4:8;
u = a * w by A1, A3, RLSUB_1:14;
hence u in W1 by RLVECT_4:8; :: thesis: verum
end;
hence Lin {w} = Lin {v} by RLSUB_1:31; :: thesis: verum