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 A6, RLSUB_1: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;

u1 = (v1 + v2) - u2 by A3, Lm14

.= v1 + (v2 - u2) by RLVECT_1:def 3 ;

then A9: u1 in C2 by A7;

u1 in C1 by A5, STRUCT_0:def 5;

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

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 A6, RLSUB_1: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;

u1 = (v1 + v2) - u2 by A3, Lm14

.= v1 + (v2 - u2) by RLVECT_1:def 3 ;

then A9: u1 in C2 by A7;

u1 in C1 by A5, STRUCT_0:def 5;

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