let V be RealUnitarySpace; :: thesis: for W1, W2 being strict Subspace of V
for u, v being VECTOR of V st v + W1 = u + W2 holds
W1 = W2
let W1, W2 be strict Subspace of V; :: thesis: for u, v being VECTOR of V st v + W1 = u + W2 holds
W1 = W2
let u, v be VECTOR of V; :: thesis: ( v + W1 = u + W2 implies W1 = W2 )
assume A1: v + W1 = u + W2 ; :: thesis: W1 = W2
set V1 = the carrier of W1;
set V2 = the carrier of W2;
assume A2: W1 <> W2 ; :: thesis: contradiction
then the carrier of W1 <> the carrier of W2 by Th24;
then A3: ( 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;

A4: now

assume A5: the carrier of W1 \ the carrier of W2 <> {} ; :: thesis: contradiction
consider x being Element of the carrier of W1 \ the carrier of W2;
( x in the carrier of W1 & not x in the carrier of W2 ) by A5, XBOOLE_0:def 5;
then A6: ( x in W1 & not x in W2 ) by STRUCT_0:def 5;
then x in V by Th2;
then reconsider x = x as Element of V by STRUCT_0:def 5;
set z = v + x;
v + x in u + W2 by A1, A6;
then consider u1 being VECTOR of V such that
A7: v + x = u + u1 and
A8: u1 in W2 ;
x = (0. V) + x by RLVECT_1:10
.= (v - v) + x by RLVECT_1:28
.= (- v) + (u + u1) by A7, RLVECT_1:def 6 ;
then A9: (v + ((- v) + (u + u1))) + W1 = v + W1 by A6, Th46;
v + ((- v) + (u + u1)) = (v - v) + (u + u1) by RLVECT_1:def 6
.= (0. V) + (u + u1) by RLVECT_1:28
.= u + u1 by RLVECT_1:10 ;
then (u + u1) + W2 = (u + u1) + W1 by A1, A8, A9, Th46;
hence contradiction by A2, Th62; :: thesis: verum

end;

now

assume A10: the carrier of W2 \ the carrier of W1 <> {} ; :: thesis: contradiction
consider x being Element of the carrier of W2 \ the carrier of W1;
( x in the carrier of W2 & not x in the carrier of W1 ) by A10, XBOOLE_0:def 5;
then A11: ( x in W2 & not x in W1 ) by STRUCT_0:def 5;
then x in V by Th2;
then reconsider x = x as Element of V by STRUCT_0:def 5;
set z = u + x;
u + x in v + W1 by A1, A11;
then consider u1 being VECTOR of V such that
A12: u + x = v + u1 and
A13: u1 in W1 ;
x = (0. V) + x by RLVECT_1:10
.= (u - u) + x by RLVECT_1:28
.= (- u) + (v + u1) by A12, RLVECT_1:def 6 ;
then A14: (u + ((- u) + (v + u1))) + W2 = u + W2 by A11, Th46;
u + ((- u) + (v + u1)) = (u - u) + (v + u1) by RLVECT_1:def 6
.= (0. V) + (v + u1) by RLVECT_1:28
.= v + u1 by RLVECT_1:10 ;
then (v + u1) + W1 = (v + u1) + W2 by A1, A13, A14, Th46;
hence contradiction by A2, Th62; :: thesis: verum

end;

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