let V be Z_Module; :: thesis: for W being Submodule 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 Submodule 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 Z_Module ;

A1: B9 is Submodule of V9 by ZMODUL01:42;

assume A2: A = B ; :: thesis: Lin A = Lin B

hence Lin A = Lin B by A1, A6, XBOOLE_0:def 10, ZMODUL01:45; :: 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 Submodule 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 Z_Module ;

A1: B9 is Submodule of V9 by ZMODUL01:42;

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 consider L being Linear_Combination of A such that

A3: x = Sum L by STRUCT_0:def 5, ZMODUL02:64;

Carrier L c= A by VECTSP_6:def 4;

then consider K being Linear_Combination of W such that

A4: Carrier K = Carrier L and

A5: Sum K = Sum L by A2, Th13, XBOOLE_1:1;

reconsider K = K as Linear_Combination of B by A2, A4, VECTSP_6:def 4;

x = Sum K by A3, A5;

hence x in the carrier of (Lin B) by STRUCT_0:def 5, ZMODUL02:64; :: thesis: verum

end;assume x in the carrier of (Lin A) ; :: thesis: x in the carrier of (Lin B)

then consider L being Linear_Combination of A such that

A3: x = Sum L by STRUCT_0:def 5, ZMODUL02:64;

Carrier L c= A by VECTSP_6:def 4;

then consider K being Linear_Combination of W such that

A4: Carrier K = Carrier L and

A5: Sum K = Sum L by A2, Th13, XBOOLE_1:1;

reconsider K = K as Linear_Combination of B by A2, A4, VECTSP_6:def 4;

x = Sum K by A3, A5;

hence x in the carrier of (Lin B) by STRUCT_0:def 5, ZMODUL02:64; :: 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 consider K being Linear_Combination of B such that

A7: x = Sum K by STRUCT_0:def 5, ZMODUL02:64;

consider L being Linear_Combination of V such that

A8: Carrier L = Carrier K and

A9: Sum L = Sum K by Th12;

reconsider L = L as Linear_Combination of A by A2, A8, VECTSP_6:def 4;

x = Sum L by A7, A9;

hence x in the carrier of (Lin A) by STRUCT_0:def 5, ZMODUL02:64; :: thesis: verum

end;assume x in the carrier of (Lin B) ; :: thesis: x in the carrier of (Lin A)

then consider K being Linear_Combination of B such that

A7: x = Sum K by STRUCT_0:def 5, ZMODUL02:64;

consider L being Linear_Combination of V such that

A8: Carrier L = Carrier K and

A9: Sum L = Sum K by Th12;

reconsider L = L as Linear_Combination of A by A2, A8, VECTSP_6:def 4;

x = Sum L by A7, A9;

hence x in the carrier of (Lin A) by STRUCT_0:def 5, ZMODUL02:64; :: thesis: verum

hence Lin A = Lin B by A1, A6, XBOOLE_0:def 10, ZMODUL01:45; :: thesis: verum