let V be RealLinearSpace; :: thesis: for W1, W2 being Subspace of V
for u1, u2, v, v1, v2 being VECTOR of V st V 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 V; :: thesis: for u1, u2, v, v1, v2 being VECTOR of V st V 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 u1, u2, v, v1, v2 be VECTOR of V; :: thesis: ( V 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 RLSUB_1:def 6;
reconsider C1 = the carrier of W1 as Coset of W1 by RLSUB_1:74;
A1: v1 in C2 by RLSUB_1:43;
assume V 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 VECTOR of V such that
A2: C1 /\ C2 = {u} by Th43;
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 ;
v1 in C1 by ;
then v1 in C1 /\ C2 by ;
then A8: v1 = u by ;
u1 = (v1 + v2) - u2 by
.= v1 + (v2 - u2) by RLVECT_1:def 3 ;
then A9: u1 in C2 by A7;
u1 in C1 by ;
then A10: u1 in C1 /\ C2 by ;
hence v1 = u1 by ; :: thesis: v2 = u2
u1 = u by ;
hence v2 = u2 by ; :: thesis: verum