let E be RealLinearSpace; :: thesis: for v being Element of E
for A, B being non empty binary-image of E holds
( (v + A) (-) B = A (-) (v + B) & (v + A) (-) B = v + (A (-) B) )
let v be Element of E; :: thesis: for A, B being non empty binary-image of E holds
( (v + A) (-) B = A (-) (v + B) & (v + A) (-) B = v + (A (-) B) )
let A, B be non empty binary-image of E; :: thesis: ( (v + A) (-) B = A (-) (v + B) & (v + A) (-) B = v + (A (-) B) )
for x being set holds
( x in (v + A) (-) B iff x in A (-) (v + B) )

proof

let x be set ; :: thesis: ( x in (v + A) (-) B iff x in A (-) (v + B) )

hereby :: thesis: ( x in A (-) (v + B) implies x in (v + A) (-) B )

assume x in (v + A) (-) B ; :: thesis: x in A (-) (v + B)
then consider w being Element of E such that
P1: ( x = w & ( for b being Element of E st b in B holds
w - b in v + A ) ) ;

now :: thesis: for vb being Element of E st vb in v + B holds
w - vb in A

let vb be Element of E; :: thesis: ( vb in v + B implies w - vb in A )
assume vb in v + B ; :: thesis: w - vb in A
then consider b being Element of E such that
P3: ( vb = v + b & b in B ) ;
w - b in v + A by P3, P1;
then consider a being Element of E such that
P5: ( w - b = v + a & a in A ) ;
w - vb = (w - b) - v by P3, RLVECT_1:27
.= a by P5, RLVECT_4:1 ;
hence w - vb in A by P5; :: thesis: verum

end;

hence x in A (-) (v + B) by P1; :: thesis: verum

end;

assume x in A (-) (v + B) ; :: thesis: x in (v + A) (-) B
then consider w being Element of E such that
P1: ( x = w & ( for vb being Element of E st vb in v + B holds
w - vb in A ) ) ;

now :: thesis: for b being Element of E st b in B holds
w - b in v + A

let b be Element of E; :: thesis: ( b in B implies w - b in v + A )
assume b in B ; :: thesis: w - b in v + A
then v + b in v + B ;
then w - (v + b) in A by P1;
then P4: v + (w - (v + b)) in v + A ;
v + (w - (v + b)) = (v + w) - (v + b) by RLVECT_1:28
.= w + (v - (v + b)) by RLVECT_1:28
.= w + ((v - v) - b) by RLVECT_1:27
.= w + ((0. E) - b) by RLVECT_1:15 ;
hence w - b in v + A by RLVECT_1:14, P4; :: thesis: verum

end;

hence x in (v + A) (-) B by P1; :: thesis: verum

end;

hence (v + A) (-) B = A (-) (v + B) by TARSKI:1; :: thesis: (v + A) (-) B = v + (A (-) B)
for x being set holds
( x in (v + A) (-) B iff x in v + (A (-) B) )

proof

let x be set ; :: thesis: ( x in (v + A) (-) B iff x in v + (A (-) B) )

hereby :: thesis: ( x in v + (A (-) B) implies x in (v + A) (-) B )

assume x in (v + A) (-) B ; :: thesis: x in v + (A (-) B)
then consider w being Element of E such that
P1: ( x = w & ( for b being Element of E st b in B holds
w - b in v + A ) ) ;

now :: thesis: for b being Element of E st b in B holds
(w - v) - b in A

let b be Element of E; :: thesis: ( b in B implies (w - v) - b in A )
assume b in B ; :: thesis: (w - v) - b in A
then X2: w - b in v + A by P1;
consider a being Element of E such that
X3: ( w - b = v + a & a in A ) by X2;
(w - v) - b = w - (v + b) by RLVECT_1:27
.= (v + a) - v by RLVECT_1:27, X3
.= a by RLVECT_4:1 ;
hence (w - v) - b in A by X3; :: thesis: verum

end;

then X4: w - v in A (-) B ;
v + (w - v) = w by RLVECT_4:1;
hence x in v + (A (-) B) by P1, X4; :: thesis: verum

end;

assume x in v + (A (-) B) ; :: thesis: x in (v + A) (-) B
then consider ab being Element of E such that
X1: ( x = v + ab & ab in A (-) B ) ;
reconsider w = x as Element of E by X1;
consider d being Element of E such that
Y1: ( ab = d & ( for b being Element of E st b in B holds
d - b in A ) ) by X1;

now :: thesis: for b being Element of E st b in B holds
(v + ab) - b in v + A

let b be Element of E; :: thesis: ( b in B implies (v + ab) - b in v + A )
assume b in B ; :: thesis: (v + ab) - b in v + A
then X2: ab - b in A by Y1;
(v + ab) - b = v + (ab - b) by RLVECT_1:28;
hence (v + ab) - b in v + A by X2; :: thesis: verum

end;

hence x in (v + A) (-) B by X1; :: thesis: verum

end;

hence (v + A) (-) B = v + (A (-) B) by TARSKI:1; :: thesis: verum