let E, L be Z_Module; 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; 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; 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; ( 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 #)
; 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; verum