let V be RealLinearSpace; :: thesis: for W being Subspace of V
for A being Subset of V
for B being Subset of W st A = B holds
Lin A = Lin B
let W be Subspace of V; :: thesis: for A being Subset of V
for B being Subset of W st A = B holds
Lin A = Lin B
let A be Subset of V; :: thesis: for B being Subset of W st A = B holds
Lin A = Lin B
let B be Subset of W; :: thesis: ( A = B implies Lin A = Lin B )
assume A1: A = B ; :: thesis: Lin A = Lin B

now

let x be set ; :: thesis: ( x in the carrier of (Lin A) implies x in the carrier of (Lin B) )
assume x in the carrier of (Lin A) ; :: thesis: x in the carrier of (Lin B)
then x in Lin A by STRUCT_0:def 5;
then consider L being Linear_Combination of A such that
A2: x = Sum L by RLVECT_3:17;
( Carrier L c= A & A c= the carrier of W ) by A1, RLVECT_2:def 8;
then Carrier L c= the carrier of W by XBOOLE_1:1;
then consider K being Linear_Combination of W such that
A3: ( Carrier K = Carrier L & Sum K = Sum L ) by Th13;
reconsider K = K as Linear_Combination of B by A1, A3, RLVECT_2:def 8;
x = Sum K by A2, A3;
then x in Lin B by RLVECT_3:17;
hence x in the carrier of (Lin B) by STRUCT_0:def 5; :: thesis: verum

end;

then A4: the carrier of (Lin A) c= the carrier of (Lin B) by TARSKI:def 3;

now

let x be set ; :: thesis: ( x in the carrier of (Lin B) implies x in the carrier of (Lin A) )
assume x in the carrier of (Lin B) ; :: thesis: x in the carrier of (Lin A)
then x in Lin B by STRUCT_0:def 5;
then consider K being Linear_Combination of B such that
A5: x = Sum K by RLVECT_3:17;
consider L being Linear_Combination of V such that
A6: ( Carrier L = Carrier K & Sum L = Sum K ) by Th12;
reconsider L = L as Linear_Combination of A by A1, A6, RLVECT_2:def 8;
x = Sum L by A5, A6;
then x in Lin A by RLVECT_3:17;
hence x in the carrier of (Lin A) by STRUCT_0:def 5; :: thesis: verum

end;

then the carrier of (Lin B) c= the carrier of (Lin A) by TARSKI:def 3;
then A7: the carrier of (Lin A) = the carrier of (Lin B) by A4, XBOOLE_0:def 10;
reconsider B' = Lin B, V' = V as RealLinearSpace ;
B' is Subspace of V' by RLSUB_1:35;
hence Lin A = Lin B by A7, RLSUB_1:38; :: thesis: verum