let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for M being non empty right_complementable VectSp-like Abelian add-associative right_zeroed VectSpStr of GF
for W1, W2 being Subspace of M st M = W1 + W2 & ex v being Element of M st
for v1, v2, u1, u2 being Element of M 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
M is_the_direct_sum_of W1,W2
let M be non empty right_complementable VectSp-like Abelian add-associative right_zeroed VectSpStr of GF; :: thesis: for W1, W2 being Subspace of M st M = W1 + W2 & ex v being Element of M st
for v1, v2, u1, u2 being Element of M 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
M is_the_direct_sum_of W1,W2
let W1, W2 be Subspace of M; :: thesis: ( M = W1 + W2 & ex v being Element of M st
for v1, v2, u1, u2 being Element of M 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 M is_the_direct_sum_of W1,W2 )
assume A1: M = W1 + W2 ; :: thesis: ( for v being Element of M ex v1, v2, u1, u2 being Element of M 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 M is_the_direct_sum_of W1,W2 )
given v being Element of M such that A2: for v1, v2, u1, u2 being Element of M 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: M is_the_direct_sum_of W1,W2
A3: the carrier of ((0). M) = {(0. M)} by VECTSP_4:def 3;
assume not M is_the_direct_sum_of W1,W2 ; :: thesis: contradiction
then W1 /\ W2 <> (0). M by A1, Def4;
then ( the carrier of (W1 /\ W2) <> the carrier of ((0). M) & (0). M is Subspace of W1 /\ W2 ) by VECTSP_4:37, VECTSP_4:50;
then ( the carrier of (W1 /\ W2) <> {(0. M)} & {(0. M)} c= the carrier of (W1 /\ W2) ) by A3, VECTSP_4:def 2;
then {(0. M)} c< the carrier of (W1 /\ W2) by XBOOLE_0:def 8;
then consider x being set such that
A4: x in the carrier of (W1 /\ W2) and
A5: not x in {(0. M)} by XBOOLE_0:6;
A6: x in W1 /\ W2 by A4, STRUCT_0:def 5;
then A7: ( x in W1 & x in W2 ) by Th7;
A8: x <> 0. M by A5, TARSKI:def 1;
x in M by A6, VECTSP_4:17;
then reconsider u = x as Element of M by STRUCT_0:def 5;
consider v1, v2 being Element of M such that
A9: ( v1 in W1 & v2 in W2 ) and
A10: v = v1 + v2 by A1, Lm16;
A11: v = (v1 + v2) + (0. M) by A10, RLVECT_1:10
.= (v1 + v2) + (u - u) by VECTSP_1:66
.= ((v1 + v2) + u) - u by RLVECT_1:def 6
.= ((v1 + u) + v2) - u by RLVECT_1:def 6
.= (v1 + u) + (v2 - u) by RLVECT_1:def 6 ;
( v1 + u in W1 & v2 - u in W2 ) by A7, A9, VECTSP_4:28, VECTSP_4:31;
then v2 - u = v2 by A2, A9, A10, A11;
then v2 + (- u) = v2 + (0. M) by RLVECT_1:10;
then - u = 0. M by RLVECT_1:21;
then u = - (0. M) by RLVECT_1:30;
hence contradiction by A8, RLVECT_1:25; :: thesis: verum