let R be Ring; for V being RightMod of R
for W1, W2 being Submodule 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 be RightMod of R; for W1, W2 being Submodule 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 Submodule 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 RMOD_2:def 6;
reconsider C1 = the carrier of W1 as Coset of W1 by RMOD_2:70;
A1:
v1 in C2
by RMOD_2:44;
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 Th41;
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, RMOD_2:23;
v1 in C1
by A4;
then
v1 in C1 /\ C2
by A1, XBOOLE_0:def 4;
then A8:
v1 = u
by A2, TARSKI:def 1;
u1 =
(v1 + v2) - u2
by A3, Lm15
.=
v1 + (v2 - u2)
by RLVECT_1:def 3
;
then A9:
u1 in C2
by A7;
u1 in C1
by A5;
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