let V be RealLinearSpace; :: thesis: for u, v being VECTOR of V
for W1, W2 being strict Subspace of V st v + W1 = u + W2 holds
W1 = W2
let u, v be VECTOR 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 VECTOR of V such that
A5: v + x = u + u1 and
A6: u1 in W2 ;
x = (0. V) + x
.= (v - v) + x by RLVECT_1:15
.= (- v) + (u + u1) by A5, RLVECT_1:def 3 ;
then A7: (v + ((- v) + (u + u1))) + W1 = v + W1 by A4, Th52;
v + ((- v) + (u + u1)) = (v - v) + (u + u1) by RLVECT_1:def 3
.= (0. V) + (u + u1) by RLVECT_1:15
.= u + u1 ;
then (u + u1) + W2 = (u + u1) + W1 by A1, A6, A7, Th52;
hence contradiction by A2, Th68; :: 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 VECTOR of V such that
A10: u + x = v + u1 and
A11: u1 in W1 ;
x = (0. V) + x
.= (u - u) + x by RLVECT_1:15
.= (- u) + (v + u1) by A10, RLVECT_1:def 3 ;
then A12: (u + ((- u) + (v + u1))) + W2 = u + W2 by A9, Th52;
u + ((- u) + (v + u1)) = (u - u) + (v + u1) by RLVECT_1:def 3
.= (0. V) + (v + u1) by RLVECT_1:15
.= v + u1 ;
then (v + u1) + W1 = (v + u1) + W2 by A1, A11, A12, Th52;
hence contradiction by A2, Th68; :: thesis: verum
end;
the carrier of W1 <> the carrier of W2 by A2, Th30;
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