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
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 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;
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 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;
then the carrier of (Lin B) c= the carrier of (Lin A) ;
hence Lin A = Lin B by A1, A6, XBOOLE_0:def 10, ZMODUL01:45; :: thesis: verum