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

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

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)

then A6:
the carrier of (Lin A) c= the carrier of (Lin B)
;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;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

now :: thesis: for x being object st x in the carrier of (Lin B) holds

x in the carrier of (Lin A)

then
the carrier of (Lin B) c= the carrier of (Lin A)
;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;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

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