let K be Field; for V being VectSp of K
for W1, W2 being 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 V be VectSp of K; for W1, W2 being 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 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 I1 be Basis of W1; for I2 being Basis of W2 st V is_the_direct_sum_of W1,W2 holds
I1 /\ I2 = {}
let I2 be Basis of W2; ( V is_the_direct_sum_of W1,W2 implies I1 /\ I2 = {} )
assume A1:
V is_the_direct_sum_of W1,W2
; I1 /\ I2 = {}
assume
I1 /\ I2 <> {}
; 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 VECTSP_7:2, VECTSP_7:def 3;
then A4:
v <> 0. V
by A3, VECTSP_4:11;
A5:
v in W1
by A3;
v in W2
by A2;
then
v in W1 /\ W2
by A5, VECTSP_5:3;
then
v in (0). V
by A1, VECTSP_5:def 4;
hence
contradiction
by A4, VECTSP_4:35; verum