let V be RealUnitarySpace; :: thesis: for W1, W2 being Subspace of V
for v, v1, v2, u1, u2 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 v, v1, v2, u1, u2 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 v, v1, v2, u1, u2 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 ) )
assume A1: 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 ) )
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 RUSUB_1:def 5;
reconsider C1 = the carrier of W1 as Coset of W1 by RUSUB_1:68;
A5: u1 = (v1 + v2) - u2 by A2, RLSUB_2:78
.= v1 + (v2 - u2) by RLVECT_1:def 6 ;
v2 - u2 in W2 by A4, RUSUB_1:17;
then ( v1 in C1 & v1 in C2 & u1 in C1 & u1 in C2 ) by A3, A5, Lm16, RUSUB_1:37, STRUCT_0:def 5;
then A6: ( v1 in C1 /\ C2 & u1 in C1 /\ C2 ) by XBOOLE_0:def 4;
consider u being VECTOR of V such that
A7: C1 /\ C2 = {u} by A1, Th43;
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