let V be RealLinearSpace; :: thesis: for v being VECTOR of V
for W1, W2 being strict Subspace of V holds
( v + W1 = v + W2 iff W1 = W2 )
let v be VECTOR 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 VECTOR of V such that
A4: v + y = v + u and
A5: u in W2 ;
y = u by A4, RLVECT_1:8;
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 VECTOR of V such that
A7: v + y = v + u and
A8: u in W1 ;
y = u by A7, RLVECT_1:8;
hence x in the carrier of W1 by A8; :: thesis: verum

end;

hence W1 = W2 by Th30; :: thesis: verum

end;

thus ( W1 = W2 implies v + W1 = v + W2 ) ; :: thesis: verum