let E, L be Z_Module; :: thesis: for I being Subset of L
for J being Subset of E
for K being Linear_Combination of J st I = J & ModuleStr(# the carrier of L, the addF of L, the ZeroF of L, the lmult of L #) = ModuleStr(# the carrier of E, the addF of E, the ZeroF of E, the lmult of E #) holds
K is Linear_Combination of I
let I be Subset of L; :: thesis: for J being Subset of E
for K being Linear_Combination of J st I = J & ModuleStr(# the carrier of L, the addF of L, the ZeroF of L, the lmult of L #) = ModuleStr(# the carrier of E, the addF of E, the ZeroF of E, the lmult of E #) holds
K is Linear_Combination of I
let J be Subset of E; :: thesis: for K being Linear_Combination of J st I = J & ModuleStr(# the carrier of L, the addF of L, the ZeroF of L, the lmult of L #) = ModuleStr(# the carrier of E, the addF of E, the ZeroF of E, the lmult of E #) holds
K is Linear_Combination of I
let K be Linear_Combination of J; :: thesis: ( I = J & ModuleStr(# the carrier of L, the addF of L, the ZeroF of L, the lmult of L #) = ModuleStr(# the carrier of E, the addF of E, the ZeroF of E, the lmult of E #) implies K is Linear_Combination of I )
assume that
AS1: I = J and
AS2: ModuleStr(# the carrier of L, the addF of L, the ZeroF of L, the lmult of L #) = ModuleStr(# the carrier of E, the addF of E, the ZeroF of E, the lmult of E #) ; :: thesis: K is Linear_Combination of I
P1: ( K is Linear_Combination of E & Carrier K c= J ) by VECTSP_6:def 4;
consider T being finite Subset of E such that
P4: for v being Element of E st not v in T holds
K . v = 0. INT.Ring by VECTSP_6:def 1;
reconsider S = T as finite Subset of L by AS2;
reconsider H = K as Linear_Combination of L by AS2, P4, VECTSP_6:def 1;
Carrier H c= I by P1, AS1, AS2;
hence K is Linear_Combination of I by VECTSP_6:def 4; :: thesis: verum