let V be RealUnitarySpace; 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; 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; ( 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 RUSUB_1:def 5;
reconsider C1 = the carrier of W1 as Coset of W1 by RUSUB_1:68;
A1:
v1 in C2
by RUSUB_1:37;
assume
V is_the_direct_sum_of W1,W2
; ( 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 )
; ( v1 = u1 & v2 = u2 )
A7:
v2 - u2 in W2
by A6, RUSUB_1:17;
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, RLSUB_2:61
.=
v1 + (v2 - u2)
by RLVECT_1:def 3
;
then
u1 in C2
by A7, Lm16;
then A10:
u1 in C1 /\ C2
by A9, XBOOLE_0:def 4;
hence
v1 = u1
by A2, A8, TARSKI:def 1; v2 = u2
u1 = u
by A10, A2, TARSKI:def 1;
hence
v2 = u2
by A3, A8, RLVECT_1:8; verum