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
proof
let E,
L be
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 let I be
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 J be
Subset of
E;
( 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
;
J is linearly-independent
for
K being
Linear_Combination of
J st
Sum K = 0. E holds
Carrier K = {}
hence
J is
linearly-independent
by VECTSP_7:def 1;
verum
end;
hence
for L, E being Z_Module
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 )
; verum