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 )
reconsider B9 = Lin B, V9 = V as RealLinearSpace ;
A1: B9 is Subspace of V9 by RLSUB_1:27;
assume A2: A = B ; :: thesis: Lin A = Lin B
now :: thesis: for x being object st x in the carrier of (Lin A) holds
x in the carrier of (Lin B)
let x be object ; :: 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
A3: x = Sum L by RLVECT_3:14;
Carrier L c= A by RLVECT_2:def 6;
then consider K being Linear_Combination of W such that
A4: Carrier K = Carrier L and
A5: Sum K = Sum L by A2, Th12, XBOOLE_1:1;
reconsider K = K as Linear_Combination of B by A2, A4, RLVECT_2:def 6;
x = Sum K by A3, A5;
then x in Lin B by RLVECT_3:14;
hence x in the carrier of (Lin B) by STRUCT_0:def 5; :: thesis: verum
end;
then A6: the carrier of (Lin A) c= the carrier of (Lin B) ;
now :: thesis: for x being object st x in the carrier of (Lin B) holds
x in the carrier of (Lin A)
let x be object ; :: 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
A7: x = Sum K by RLVECT_3:14;
consider L being Linear_Combination of V such that
A8: Carrier L = Carrier K and
A9: Sum L = Sum K by Th11;
reconsider L = L as Linear_Combination of A by A2, A8, RLVECT_2:def 6;
x = Sum L by A7, A9;
then x in Lin A by RLVECT_3:14;
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) ;
then the carrier of (Lin A) = the carrier of (Lin B) by A6, XBOOLE_0:def 10;
hence Lin A = Lin B by A1, RLSUB_1:30; :: thesis: verum