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
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;
A8: now :: thesis: not the carrier of W2 \ the carrier of W1 <> {}
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;
the carrier of W1 <> the carrier of W2 by A2, Th29;
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