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 object holds

( x in (v + A) (-) B iff x in A (-) (v + B) )

for x being object holds

( x in (v + A) (-) B iff x in v + (A (-) B) )

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 object holds

( x in (v + A) (-) B iff x in A (-) (v + B) )

proof

hence
(v + A) (-) B = A (-) (v + B)
by TARSKI:2; :: thesis: (v + A) (-) B = v + (A (-) B)
let x be object ; :: thesis: ( x in (v + A) (-) B iff x in A (-) (v + B) )

then consider w being Element of E such that

A4: ( x = w & ( for vb being Element of E st vb in v + B holds

w - vb in A ) ) ;

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

assume
x in A (-) (v + B)
; :: thesis: x in (v + A) (-) Bassume
x in (v + A) (-) B
; :: thesis: x in A (-) (v + B)

then consider w being Element of E such that

A1: ( x = w & ( for b being Element of E st b in B holds

w - b in v + A ) ) ;

end;then consider w being Element of E such that

A1: ( 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

hence
x in A (-) (v + B)
by A1; :: thesis: verumw - 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

A2: ( vb = v + b & b in B ) ;

w - b in v + A by A2, A1;

then consider a being Element of E such that

A3: ( w - b = v + a & a in A ) ;

w - vb = (w - b) - v by A2, RLVECT_1:27

.= a by A3, RLVECT_4:1 ;

hence w - vb in A by A3; :: thesis: verum

end;assume vb in v + B ; :: thesis: w - vb in A

then consider b being Element of E such that

A2: ( vb = v + b & b in B ) ;

w - b in v + A by A2, A1;

then consider a being Element of E such that

A3: ( w - b = v + a & a in A ) ;

w - vb = (w - b) - v by A2, RLVECT_1:27

.= a by A3, RLVECT_4:1 ;

hence w - vb in A by A3; :: thesis: verum

then consider w being Element of E such that

A4: ( 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

hence
x in (v + A) (-) B
by A4; :: thesis: verumw - 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 A4;

then A5: 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 A5; :: thesis: verum

end;assume b in B ; :: thesis: w - b in v + A

then v + b in v + B ;

then w - (v + b) in A by A4;

then A5: 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 A5; :: thesis: verum

for x being object holds

( x in (v + A) (-) B iff x in v + (A (-) B) )

proof

hence
(v + A) (-) B = v + (A (-) B)
by TARSKI:2; :: thesis: verum
let x be object ; :: thesis: ( x in (v + A) (-) B iff x in v + (A (-) B) )

then consider ab being Element of E such that

A10: ( x = v + ab & ab in A (-) B ) ;

reconsider w = x as Element of E by A10;

consider d being Element of E such that

A11: ( ab = d & ( for b being Element of E st b in B holds

d - b in A ) ) by A10;

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

assume
x in v + (A (-) B)
; :: thesis: x in (v + A) (-) Bassume
x in (v + A) (-) B
; :: thesis: x in v + (A (-) B)

then consider w being Element of E such that

A6: ( x = w & ( for b being Element of E st b in B holds

w - b in v + A ) ) ;

v + (w - v) = w by RLVECT_4:1;

hence x in v + (A (-) B) by A6, A9; :: thesis: verum

end;then consider w being Element of E such that

A6: ( 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

then A9:
w - v in A (-) B
;(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 A7: w - b in v + A by A6;

consider a being Element of E such that

A8: ( w - b = v + a & a in A ) by A7;

(w - v) - b = w - (v + b) by RLVECT_1:27

.= (v + a) - v by A8, RLVECT_1:27

.= a by RLVECT_4:1 ;

hence (w - v) - b in A by A8; :: thesis: verum

end;assume b in B ; :: thesis: (w - v) - b in A

then A7: w - b in v + A by A6;

consider a being Element of E such that

A8: ( w - b = v + a & a in A ) by A7;

(w - v) - b = w - (v + b) by RLVECT_1:27

.= (v + a) - v by A8, RLVECT_1:27

.= a by RLVECT_4:1 ;

hence (w - v) - b in A by A8; :: thesis: verum

v + (w - v) = w by RLVECT_4:1;

hence x in v + (A (-) B) by A6, A9; :: thesis: verum

then consider ab being Element of E such that

A10: ( x = v + ab & ab in A (-) B ) ;

reconsider w = x as Element of E by A10;

consider d being Element of E such that

A11: ( ab = d & ( for b being Element of E st b in B holds

d - b in A ) ) by A10;

now :: thesis: for b being Element of E st b in B holds

(v + ab) - b in v + A

hence
x in (v + A) (-) B
by A10; :: thesis: verum(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 A12: ab - b in A by A11;

(v + ab) - b = v + (ab - b) by RLVECT_1:28;

hence (v + ab) - b in v + A by A12; :: thesis: verum

end;assume b in B ; :: thesis: (v + ab) - b in v + A

then A12: ab - b in A by A11;

(v + ab) - b = v + (ab - b) by RLVECT_1:28;

hence (v + ab) - b in v + A by A12; :: thesis: verum