let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr of GF
for v, u being Element of V
for W1, W2 being strict Subspace of V st v + W1 = u + W2 holds
W1 = W2
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr of GF; :: thesis: for v, u being Element of V
for W1, W2 being strict Subspace of V st v + W1 = u + W2 holds
W1 = W2
let v, u be Element of V; :: thesis: for W1, W2 being strict Subspace of V st v + W1 = u + W2 holds
W1 = W2
let W1, W2 be strict Subspace of V; :: thesis: ( v + W1 = u + W2 implies W1 = W2 )
assume A1: v + W1 = u + W2 ; :: thesis: W1 = W2
set V2 = the carrier of W2;
set V1 = the carrier of W1;
assume A2: W1 <> W2 ; :: thesis: contradiction

A3: now

set x = the Element of the carrier of W1 \ the carrier of W2;
assume the carrier of W1 \ the carrier of W2 <> {} ; :: thesis: contradiction
then the Element of the carrier of W1 \ the carrier of W2 in the carrier of W1 by XBOOLE_0:def 5;
then A4: the Element of the carrier of W1 \ the carrier of W2 in W1 by STRUCT_0:def 5;
then the Element of the carrier of W1 \ the carrier of W2 in V by Th17;
then reconsider x = the Element of the carrier of W1 \ the carrier of W2 as Element of V by STRUCT_0:def 5;
set z = v + x;
v + x in u + W2 by A1, A4;
then consider u1 being Element of V such that
A5: v + x = u + u1 and
A6: u1 in W2 ;
x = (0. V) + x by RLVECT_1:4
.= (v + (- v)) + x by VECTSP_1:19
.= (- v) + (u + u1) by A5, RLVECT_1:def 3 ;
then A7: (v + ((- v) + (u + u1))) + W1 = v + W1 by A4, Th68;
v + ((- v) + (u + u1)) = (v + (- v)) + (u + u1) by RLVECT_1:def 3
.= (0. V) + (u + u1) by VECTSP_1:19
.= u + u1 by RLVECT_1:4 ;
then (u + u1) + W2 = (u + u1) + W1 by A1, A6, A7, Th68;
hence contradiction by A2, Th82; :: thesis: verum

end;

A8: now

set x = the Element of the carrier of W2 \ the carrier of W1;
assume the carrier of W2 \ the carrier of W1 <> {} ; :: thesis: contradiction
then the Element of the carrier of W2 \ the carrier of W1 in the carrier of W2 by XBOOLE_0:def 5;
then A9: the Element of the carrier of W2 \ the carrier of W1 in W2 by STRUCT_0:def 5;
then the Element of the carrier of W2 \ the carrier of W1 in V by Th17;
then reconsider x = the Element of the carrier of W2 \ the carrier of W1 as Element of V by STRUCT_0:def 5;
set z = u + x;
u + x in v + W1 by A1, A9;
then consider u1 being Element of V such that
A10: u + x = v + u1 and
A11: u1 in W1 ;
x = (0. V) + x by RLVECT_1:4
.= (u + (- u)) + x by VECTSP_1:19
.= (- u) + (v + u1) by A10, RLVECT_1:def 3 ;
then A12: (u + ((- u) + (v + u1))) + W2 = u + W2 by A9, Th68;
u + ((- u) + (v + u1)) = (u + (- u)) + (v + u1) by RLVECT_1:def 3
.= (0. V) + (v + u1) by VECTSP_1:19
.= v + u1 by RLVECT_1:4 ;
then (v + u1) + W1 = (v + u1) + W2 by A1, A11, A12, Th68;
hence contradiction by A2, Th82; :: thesis: verum

end;

the carrier of W1 <> the carrier of W2 by A2, Th37;
then ( not the carrier of W1 c= the carrier of W2 or not the carrier of W2 c= the carrier of W1 ) by XBOOLE_0:def 10;
hence contradiction by A3, A8, XBOOLE_1:37; :: thesis: verum