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

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