let V be RealLinearSpace; :: thesis: for W1, W2 being Subspace of V st V = W1 + W2 & ex v being VECTOR of V st

for v1, v2, u1, u2 being VECTOR of V st v = v1 + v2 & v = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 holds

( v1 = u1 & v2 = u2 ) holds

V is_the_direct_sum_of W1,W2

let W1, W2 be Subspace of V; :: thesis: ( V = W1 + W2 & ex v being VECTOR of V st

for v1, v2, u1, u2 being VECTOR of V st v = v1 + v2 & v = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 holds

( v1 = u1 & v2 = u2 ) implies V is_the_direct_sum_of W1,W2 )

assume A1: V = W1 + W2 ; :: thesis: ( for v being VECTOR of V ex v1, v2, u1, u2 being VECTOR of V st

( v = v1 + v2 & v = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 & not ( v1 = u1 & v2 = u2 ) ) or V is_the_direct_sum_of W1,W2 )

( the carrier of ((0). V) = {(0. V)} & (0). V is Subspace of W1 /\ W2 ) by RLSUB_1:39, RLSUB_1:def 3;

then A2: {(0. V)} c= the carrier of (W1 /\ W2) by RLSUB_1:def 2;

given v being VECTOR of V such that A3: for v1, v2, u1, u2 being VECTOR of V st v = v1 + v2 & v = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 holds

( v1 = u1 & v2 = u2 ) ; :: thesis: V is_the_direct_sum_of W1,W2

assume not V is_the_direct_sum_of W1,W2 ; :: thesis: contradiction

then W1 /\ W2 <> (0). V by A1;

then the carrier of (W1 /\ W2) <> {(0. V)} by RLSUB_1:def 3;

then {(0. V)} c< the carrier of (W1 /\ W2) by A2;

then consider x being object such that

A4: x in the carrier of (W1 /\ W2) and

A5: not x in {(0. V)} by XBOOLE_0:6;

A6: x <> 0. V by A5, TARSKI:def 1;

A7: x in W1 /\ W2 by A4, STRUCT_0:def 5;

then x in V by RLSUB_1:9;

then reconsider u = x as VECTOR of V by STRUCT_0:def 5;

consider v1, v2 being VECTOR of V such that

A8: v1 in W1 and

A9: v2 in W2 and

A10: v = v1 + v2 by A1, Lm13;

A11: v = (v1 + v2) + (0. V) by A10

.= (v1 + v2) + (u - u) by RLVECT_1:15

.= ((v1 + v2) + u) - u by RLVECT_1:def 3

.= ((v1 + u) + v2) - u by RLVECT_1:def 3

.= (v1 + u) + (v2 - u) by RLVECT_1:def 3 ;

x in W2 by A7, Th3;

then A12: v2 - u in W2 by A9, RLSUB_1:23;

x in W1 by A7, Th3;

then v1 + u in W1 by A8, RLSUB_1:20;

then v2 - u = v2 by A3, A8, A9, A10, A11, A12

.= v2 - (0. V) ;

hence contradiction by A6, RLVECT_1:23; :: thesis: verum

for v1, v2, u1, u2 being VECTOR of V st v = v1 + v2 & v = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 holds

( v1 = u1 & v2 = u2 ) holds

V is_the_direct_sum_of W1,W2

let W1, W2 be Subspace of V; :: thesis: ( V = W1 + W2 & ex v being VECTOR of V st

for v1, v2, u1, u2 being VECTOR of V st v = v1 + v2 & v = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 holds

( v1 = u1 & v2 = u2 ) implies V is_the_direct_sum_of W1,W2 )

assume A1: V = W1 + W2 ; :: thesis: ( for v being VECTOR of V ex v1, v2, u1, u2 being VECTOR of V st

( v = v1 + v2 & v = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 & not ( v1 = u1 & v2 = u2 ) ) or V is_the_direct_sum_of W1,W2 )

( the carrier of ((0). V) = {(0. V)} & (0). V is Subspace of W1 /\ W2 ) by RLSUB_1:39, RLSUB_1:def 3;

then A2: {(0. V)} c= the carrier of (W1 /\ W2) by RLSUB_1:def 2;

given v being VECTOR of V such that A3: for v1, v2, u1, u2 being VECTOR of V st v = v1 + v2 & v = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 holds

( v1 = u1 & v2 = u2 ) ; :: thesis: V is_the_direct_sum_of W1,W2

assume not V is_the_direct_sum_of W1,W2 ; :: thesis: contradiction

then W1 /\ W2 <> (0). V by A1;

then the carrier of (W1 /\ W2) <> {(0. V)} by RLSUB_1:def 3;

then {(0. V)} c< the carrier of (W1 /\ W2) by A2;

then consider x being object such that

A4: x in the carrier of (W1 /\ W2) and

A5: not x in {(0. V)} by XBOOLE_0:6;

A6: x <> 0. V by A5, TARSKI:def 1;

A7: x in W1 /\ W2 by A4, STRUCT_0:def 5;

then x in V by RLSUB_1:9;

then reconsider u = x as VECTOR of V by STRUCT_0:def 5;

consider v1, v2 being VECTOR of V such that

A8: v1 in W1 and

A9: v2 in W2 and

A10: v = v1 + v2 by A1, Lm13;

A11: v = (v1 + v2) + (0. V) by A10

.= (v1 + v2) + (u - u) by RLVECT_1:15

.= ((v1 + v2) + u) - u by RLVECT_1:def 3

.= ((v1 + u) + v2) - u by RLVECT_1:def 3

.= (v1 + u) + (v2 - u) by RLVECT_1:def 3 ;

x in W2 by A7, Th3;

then A12: v2 - u in W2 by A9, RLSUB_1:23;

x in W1 by A7, Th3;

then v1 + u in W1 by A8, RLSUB_1:20;

then v2 - u = v2 by A3, A8, A9, A10, A11, A12

.= v2 - (0. V) ;

hence contradiction by A6, RLVECT_1:23; :: thesis: verum