let V be Z_Module; :: thesis: for I, I1 being linearly-independent Subset of V st I1 c= I holds
(Lin (I \ I1)) /\ (Lin I1) = (0). V
let I, I1 be linearly-independent Subset of V; :: thesis: ( I1 c= I implies (Lin (I \ I1)) /\ (Lin I1) = (0). V )
assume A1: I1 c= I ; :: thesis: (Lin (I \ I1)) /\ (Lin I1) = (0). V
assume (Lin (I \ I1)) /\ (Lin I1) <> (0). V ; :: thesis: contradiction
then consider v being Vector of V such that
A2: ( v in (Lin (I \ I1)) /\ (Lin I1) & v <> 0. V ) by ZMODUL04:24;
v in Lin (I \ I1) by A2, ZMODUL01:94;
then consider l1 being Linear_Combination of I \ I1 such that
A3: v = Sum l1 by ZMODUL02:64;
A4: Carrier l1 c= I \ I1 by VECTSP_6:def 4;
v in Lin I1 by A2, ZMODUL01:94;
then consider l2 being Linear_Combination of I1 such that
A5: v = Sum l2 by ZMODUL02:64;
A6: Carrier l2 c= I1 by VECTSP_6:def 4;
reconsider ll1 = l1 as Linear_Combination of I by XBOOLE_1:36, ZMODUL02:10;
reconsider ll2 = l2 as Linear_Combination of I by A1, ZMODUL02:10;
Carrier l1 misses Carrier l2 by A4, A6, XBOOLE_1:64, XBOOLE_1:79;
then (Carrier ll1) /\ (Carrier ll2) = {} by XBOOLE_0:def 7;
then A10: (Carrier ll1) /\ (Carrier (- ll2)) = {} by ZMODUL02:37;
reconsider ll2x = - ll2 as Linear_Combination of I by ZMODUL02:38;
A7: Carrier (ll1 - ll2) = (Carrier ll1) \/ (Carrier ll2x) by A10, ZMODUL04:25;
A8: (Sum ll1) - (Sum ll2) = 0. V by A3, A5, RLVECT_1:5;
reconsider l = ll1 - ll2 as Linear_Combination of I by ZMODUL02:41;
A9: Sum l = 0. V by A8, ZMODUL02:55;
Carrier ll1 <> {} by A2, A3, ZMODUL02:23;
hence contradiction by A9, A7, VECTSP_7:def 1; :: thesis: verum