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 v being Element of V
for W1, W2 being strict Subspace of V holds
( v + W1 = v + W2 iff 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 v being Element of V
for W1, W2 being strict Subspace of V holds
( v + W1 = v + W2 iff W1 = W2 )

let v be Element of V; :: thesis: for W1, W2 being strict Subspace of V holds
( v + W1 = v + W2 iff W1 = W2 )

let W1, W2 be strict Subspace of V; :: thesis: ( v + W1 = v + W2 iff W1 = W2 )
thus ( v + W1 = v + W2 implies W1 = W2 ) :: thesis: ( W1 = W2 implies v + W1 = v + W2 )
proof
assume A1: v + W1 = v + W2 ; :: thesis: W1 = W2
the carrier of W1 = the carrier of W2
proof
A2: the carrier of W1 c= the carrier of V by Def2;
thus the carrier of W1 c= the carrier of W2 :: according to XBOOLE_0:def 10 :: thesis: the carrier of W2 c= the carrier of W1
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of W1 or x in the carrier of W2 )
assume A3: x in the carrier of W1 ; :: thesis: x in the carrier of W2
then reconsider y = x as Element of V by A2;
set z = v + y;
x in W1 by A3;
then v + y in v + W2 by A1;
then consider u being Element of V such that
A4: v + y = v + u and
A5: u in W2 ;
y = u by ;
hence x in the carrier of W2 by A5; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of W2 or x in the carrier of W1 )
assume A6: x in the carrier of W2 ; :: thesis: x in the carrier of W1
the carrier of W2 c= the carrier of V by Def2;
then reconsider y = x as Element of V by A6;
set z = v + y;
x in W2 by A6;
then v + y in v + W1 by A1;
then consider u being Element of V such that
A7: v + y = v + u and
A8: u in W1 ;
y = u by ;
hence x in the carrier of W1 by A8; :: thesis: verum
end;
hence W1 = W2 by Th29; :: thesis: verum
end;
thus ( W1 = W2 implies v + W1 = v + W2 ) ; :: thesis: verum