let V be Z_Module; :: thesis: for A1, A2 being Subset of V st A1 is linearly-independent & A2 is linearly-independent & A1 /\ A2 = {} & A1 \/ A2 is linearly-dependent holds
(Lin A1) /\ (Lin A2) <> (0). V
let A1, A2 be Subset of V; :: thesis: ( A1 is linearly-independent & A2 is linearly-independent & A1 /\ A2 = {} & A1 \/ A2 is linearly-dependent implies (Lin A1) /\ (Lin A2) <> (0). V )
assume that
A1: ( A1 is linearly-independent & A2 is linearly-independent ) and
A2: ( A1 /\ A2 = {} & A1 \/ A2 is linearly-dependent ) ; :: thesis: (Lin A1) /\ (Lin A2) <> (0). V
consider l being Linear_Combination of A1 \/ A2 such that
A3: ( Sum l = 0. V & Carrier l <> {} ) by A2;
consider l1 being Linear_Combination of A1, l2 being Linear_Combination of A2 such that
A4: l = l1 + l2 by A2, ZMODUL04:26;
A5: Sum l = (Sum l1) + (Sum l2) by ZMODUL02:52, A4;
A6: Carrier l c= (Carrier l1) \/ (Carrier l2) by A4, ZMODUL02:26;
per cases ( Carrier l1 <> {} or Carrier l2 <> {} ) by A3, A6;
suppose Carrier l1 <> {} ; :: thesis: (Lin A1) /\ (Lin A2) <> (0). V
then B2: Sum l1 <> 0. V by A1;
B3: Sum l1 = - (Sum l2) by A3, A5, RLVECT_1:6;
B4: - (Sum l2) in Lin A2 by ZMODUL01:38, ZMODUL02:64;
B5: Sum l1 in Lin A1 by ZMODUL02:64;
assume (Lin A1) /\ (Lin A2) = (0). V ; :: thesis: contradiction
hence contradiction by B2, B5, ZMODUL02:66, B3, B4, ZMODUL01:94; :: thesis: verum
end;
suppose Carrier l2 <> {} ; :: thesis: (Lin A1) /\ (Lin A2) <> (0). V
then B2: Sum l2 <> 0. V by A1;
B3: Sum l2 = - (Sum l1) by A3, A5, RLVECT_1:6;
B4: - (Sum l1) in Lin A1 by ZMODUL01:38, ZMODUL02:64;
B5: Sum l2 in Lin A2 by ZMODUL02:64;
assume (Lin A1) /\ (Lin A2) = (0). V ; :: thesis: contradiction
hence contradiction by B2, B5, ZMODUL02:66, B3, B4, ZMODUL01:94; :: thesis: verum
end;
end;