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
for v, v1, v2, u1, u2 being Element of M st M is_the_direct_sum_of W1,W2 & v = v1 + v2 & v = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 holds
( v1 = u1 & v2 = u2 )
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
for v, v1, v2, u1, u2 being Element of M st M is_the_direct_sum_of W1,W2 & v = v1 + v2 & v = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 holds
( v1 = u1 & v2 = u2 )
let W1, W2 be Subspace of M; :: thesis: for v, v1, v2, u1, u2 being Element of M st M is_the_direct_sum_of W1,W2 & v = v1 + v2 & v = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 holds
( v1 = u1 & v2 = u2 )
let v, v1, v2, u1, u2 be Element of M; :: thesis: ( M is_the_direct_sum_of W1,W2 & v = v1 + v2 & v = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 implies ( v1 = u1 & v2 = u2 ) )
assume A1: M is_the_direct_sum_of W1,W2 ; :: thesis: ( not v = v1 + v2 or not v = u1 + u2 or not v1 in W1 or not u1 in W1 or not v2 in W2 or not u2 in W2 or ( v1 = u1 & v2 = u2 ) )
assume that
A2: ( v = v1 + v2 & v = u1 + u2 ) and
A3: ( v1 in W1 & u1 in W1 ) and
A4: ( v2 in W2 & u2 in W2 ) ; :: thesis: ( v1 = u1 & v2 = u2 )
reconsider C2 = v1 + W2 as Coset of W2 by VECTSP_4:def 6;
reconsider C1 = the carrier of W1 as Coset of W1 by VECTSP_4:89;
A5: u1 = (v1 + v2) - u2 by A2, VECTSP_2:22
.= v1 + (v2 - u2) by RLVECT_1:def 6 ;
v2 - u2 in W2 by A4, VECTSP_4:31;
then ( v1 in C1 & v1 in C2 & u1 in C1 & u1 in C2 ) by A3, A5, STRUCT_0:def 5, VECTSP_4:59;
then A6: ( v1 in C1 /\ C2 & u1 in C1 /\ C2 ) by XBOOLE_0:def 4;
consider u being Element of M such that
A7: C1 /\ C2 = {u} by A1, Th56;
A8: ( v1 = u & u1 = u ) by A6, A7, TARSKI:def 1;
hence v1 = u1 ; :: thesis: v2 = u2
thus v2 = u2 by A2, A8, RLVECT_1:21; :: thesis: verum