let V be Z_Module; 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; ( I1 c= I implies (Lin (I \ I1)) /\ (Lin I1) = (0). V )
assume A1:
I1 c= I
; (Lin (I \ I1)) /\ (Lin I1) = (0). V
assume
(Lin (I \ I1)) /\ (Lin I1) <> (0). V
; 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; verum