let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ; :: thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over 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 vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over 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 ) )
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:73;
A1: v1 in C2 by VECTSP_4:44;
assume 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 ) )
then consider u being Element of M such that
A2: C1 /\ C2 = {u} by Th46;
assume that
A3: ( v = v1 + v2 & v = u1 + u2 ) and
A4: v1 in W1 and
A5: u1 in W1 and
A6: ( v2 in W2 & u2 in W2 ) ; :: thesis: ( v1 = u1 & v2 = u2 )
A7: v2 - u2 in W2 by A6, VECTSP_4:23;
v1 in C1 by A4, STRUCT_0:def 5;
then v1 in C1 /\ C2 by A1, XBOOLE_0:def 4;
then A8: v1 = u by A2, TARSKI:def 1;
A9: u1 in C1 by A5, STRUCT_0:def 5;
u1 = (v1 + v2) - u2 by A3, VECTSP_2:2
.= v1 + (v2 - u2) by RLVECT_1:def 3 ;
then u1 in C2 by A7;
then A10: u1 in C1 /\ C2 by A9, XBOOLE_0:def 4;
hence v1 = u1 by A2, A8, TARSKI:def 1; :: thesis: v2 = u2
u1 = u by A10, A2, TARSKI:def 1;
hence v2 = u2 by A3, A8, RLVECT_1:8; :: thesis: verum