let V be Z_Module; :: thesis: for W1, W2 being free Subspace of V

for I1 being Basis of W1

for I2 being Basis of W2 st V is_the_direct_sum_of W1,W2 holds

I1 /\ I2 = {}

let W1, W2 be free Subspace of V; :: thesis: for I1 being Basis of W1

for I2 being Basis of W2 st V is_the_direct_sum_of W1,W2 holds

I1 /\ I2 = {}

let I1 be Basis of W1; :: thesis: for I2 being Basis of W2 st V is_the_direct_sum_of W1,W2 holds

I1 /\ I2 = {}

let I2 be Basis of W2; :: thesis: ( V is_the_direct_sum_of W1,W2 implies I1 /\ I2 = {} )

assume A1: V is_the_direct_sum_of W1,W2 ; :: thesis: I1 /\ I2 = {}

assume I1 /\ I2 <> {} ; :: thesis: contradiction

then consider v being object such that

A2: v in I1 /\ I2 by XBOOLE_0:7;

A3: v in I1 by A2, XBOOLE_0:def 4;

not 0. W1 in I1 by ZMODUL02:57, VECTSP_7:def 3;

then A4: v <> 0. V by A3, ZMODUL01:26;

A5: v in W1 by A3;

v in W2 by A2;

then W1: v in W1 /\ W2 by A5, VECTSP_5:3;

W1 /\ W2 = (0). V by A1, VECTSP_5:def 4;

then v in (0). V by W1;

hence contradiction by A4, ZMODUL02:66; :: thesis: verum

for I1 being Basis of W1

for I2 being Basis of W2 st V is_the_direct_sum_of W1,W2 holds

I1 /\ I2 = {}

let W1, W2 be free Subspace of V; :: thesis: for I1 being Basis of W1

for I2 being Basis of W2 st V is_the_direct_sum_of W1,W2 holds

I1 /\ I2 = {}

let I1 be Basis of W1; :: thesis: for I2 being Basis of W2 st V is_the_direct_sum_of W1,W2 holds

I1 /\ I2 = {}

let I2 be Basis of W2; :: thesis: ( V is_the_direct_sum_of W1,W2 implies I1 /\ I2 = {} )

assume A1: V is_the_direct_sum_of W1,W2 ; :: thesis: I1 /\ I2 = {}

assume I1 /\ I2 <> {} ; :: thesis: contradiction

then consider v being object such that

A2: v in I1 /\ I2 by XBOOLE_0:7;

A3: v in I1 by A2, XBOOLE_0:def 4;

not 0. W1 in I1 by ZMODUL02:57, VECTSP_7:def 3;

then A4: v <> 0. V by A3, ZMODUL01:26;

A5: v in W1 by A3;

v in W2 by A2;

then W1: v in W1 /\ W2 by A5, VECTSP_5:3;

W1 /\ W2 = (0). V by A1, VECTSP_5:def 4;

then v in (0). V by W1;

hence contradiction by A4, ZMODUL02:66; :: thesis: verum