for E, L being Z_Module

for I being Subset of L

for J being Subset of E 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 #) & I is linearly-independent holds

J is linearly-independent

for I being Subset of L

for J being Subset of E st 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 #) & I = J holds

( I is linearly-independent iff J is linearly-independent ) ; :: thesis: verum

for I being Subset of L

for J being Subset of E 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 #) & I is linearly-independent holds

J is linearly-independent

proof

hence
for L, E being Z_Module
let E, L be Z_Module; :: thesis: for I being Subset of L

for J being Subset of E 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 #) & I is linearly-independent holds

J is linearly-independent

let I be Subset of L; :: thesis: for J being Subset of E 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 #) & I is linearly-independent holds

J is linearly-independent

let J be Subset of E; :: 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 #) & I is linearly-independent implies J is linearly-independent )

assume that

A1: I = J and

A3: 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 #) and

A2: I is linearly-independent ; :: thesis: J is linearly-independent

for K being Linear_Combination of J st Sum K = 0. E holds

Carrier K = {}

end;for J being Subset of E 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 #) & I is linearly-independent holds

J is linearly-independent

let I be Subset of L; :: thesis: for J being Subset of E 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 #) & I is linearly-independent holds

J is linearly-independent

let J be Subset of E; :: 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 #) & I is linearly-independent implies J is linearly-independent )

assume that

A1: I = J and

A3: 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 #) and

A2: I is linearly-independent ; :: thesis: J is linearly-independent

for K being Linear_Combination of J st Sum K = 0. E holds

Carrier K = {}

proof

hence
J is linearly-independent
by VECTSP_7:def 1; :: thesis: verum
let K be Linear_Combination of J; :: thesis: ( Sum K = 0. E implies Carrier K = {} )

assume P0: Sum K = 0. E ; :: thesis: Carrier K = {}

reconsider H = K as Linear_Combination of I by A1, A3, LmEMDetX541;

P1: Carrier K = Carrier H by A3;

Sum H = 0. L by A3, P0, LmEMDetX543;

hence Carrier K = {} by A2, P1, VECTSP_7:def 1; :: thesis: verum

end;assume P0: Sum K = 0. E ; :: thesis: Carrier K = {}

reconsider H = K as Linear_Combination of I by A1, A3, LmEMDetX541;

P1: Carrier K = Carrier H by A3;

Sum H = 0. L by A3, P0, LmEMDetX543;

hence Carrier K = {} by A2, P1, VECTSP_7:def 1; :: thesis: verum

for I being Subset of L

for J being Subset of E st 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 #) & I = J holds

( I is linearly-independent iff J is linearly-independent ) ; :: thesis: verum