let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ; :: thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for u, v 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 ModuleStr over GF; :: thesis: for u, v being Element of V

for W1, W2 being strict Subspace of V st v + W1 = u + W2 holds

W1 = W2

let u, v 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

then ( not the carrier of W1 c= the carrier of W2 or not the carrier of W2 c= the carrier of W1 ) ;

hence contradiction by A3, A8, XBOOLE_1:37; :: thesis: verum

for u, v 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 ModuleStr over GF; :: thesis: for u, v being Element of V

for W1, W2 being strict Subspace of V st v + W1 = u + W2 holds

W1 = W2

let u, v 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 :: thesis: not the carrier of W1 \ the carrier of W2 <> {}

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 ;

then the Element of the carrier of W1 \ the carrier of W2 in V by Th9;

then reconsider x = the Element of the carrier of W1 \ the carrier of W2 as Element of V ;

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, Th53;

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, Th53;

hence contradiction by A2, Th66; :: thesis: verum

end;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 ;

then the Element of the carrier of W1 \ the carrier of W2 in V by Th9;

then reconsider x = the Element of the carrier of W1 \ the carrier of W2 as Element of V ;

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, Th53;

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, Th53;

hence contradiction by A2, Th66; :: thesis: verum

A8: now :: thesis: not the carrier of W2 \ the carrier of W1 <> {}

the carrier of W1 <> the carrier of W2
by A2, Th29;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 ;

then the Element of the carrier of W2 \ the carrier of W1 in V by Th9;

then reconsider x = the Element of the carrier of W2 \ the carrier of W1 as Element of V ;

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, Th53;

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, Th53;

hence contradiction by A2, Th66; :: thesis: verum

end;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 ;

then the Element of the carrier of W2 \ the carrier of W1 in V by Th9;

then reconsider x = the Element of the carrier of W2 \ the carrier of W1 as Element of V ;

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, Th53;

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, Th53;

hence contradiction by A2, Th66; :: thesis: verum

then ( not the carrier of W1 c= the carrier of W2 or not the carrier of W2 c= the carrier of W1 ) ;

hence contradiction by A3, A8, XBOOLE_1:37; :: thesis: verum