let E be RealLinearSpace; :: thesis: for A, B, C being non empty binary-image of E holds (A (-) B) (-) C = A (-) (B (+) C)

let A, B, C be non empty binary-image of E; :: thesis: (A (-) B) (-) C = A (-) (B (+) C)

for x being object holds

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

let A, B, C be non empty binary-image of E; :: thesis: (A (-) B) (-) C = A (-) (B (+) C)

for x being object holds

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

proof

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

then consider w being Element of E such that

A4: ( x = w & ( for bc being Element of E st bc in B (+) C holds

w - bc in A ) ) ;

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

assume
x in A (-) (B (+) C)
; :: thesis: x in (A (-) B) (-) Cassume
x in (A (-) B) (-) C
; :: thesis: x in A (-) (B (+) C)

then consider w being Element of E such that

A1: ( x = w & ( for c being Element of E st c in C holds

w - c in A (-) B ) ) ;

end;then consider w being Element of E such that

A1: ( x = w & ( for c being Element of E st c in C holds

w - c in A (-) B ) ) ;

now :: thesis: for bc being Element of E st bc in B (+) C holds

w - bc in A

hence
x in A (-) (B (+) C)
by A1; :: thesis: verumw - bc in A

let bc be Element of E; :: thesis: ( bc in B (+) C implies w - bc in A )

assume bc in B (+) C ; :: thesis: w - bc in A

then consider b, c being Element of E such that

A2: ( bc = b + c & b in B & c in C ) ;

w - c in A (-) B by A1, A2;

then consider g being Element of E such that

A3: ( w - c = g & ( for b being Element of E st b in B holds

g - b in A ) ) ;

w - bc = g - b by A2, A3, RLVECT_1:27;

hence w - bc in A by A3, A2; :: thesis: verum

end;assume bc in B (+) C ; :: thesis: w - bc in A

then consider b, c being Element of E such that

A2: ( bc = b + c & b in B & c in C ) ;

w - c in A (-) B by A1, A2;

then consider g being Element of E such that

A3: ( w - c = g & ( for b being Element of E st b in B holds

g - b in A ) ) ;

w - bc = g - b by A2, A3, RLVECT_1:27;

hence w - bc in A by A3, A2; :: thesis: verum

then consider w being Element of E such that

A4: ( x = w & ( for bc being Element of E st bc in B (+) C holds

w - bc in A ) ) ;

now :: thesis: for c being Element of E st c in C holds

w - c in A (-) B

hence
x in (A (-) B) (-) C
by A4; :: thesis: verumw - c in A (-) B

let c be Element of E; :: thesis: ( c in C implies w - c in A (-) B )

assume A5: c in C ; :: thesis: w - c in A (-) B

end;assume A5: c in C ; :: thesis: w - c in A (-) B

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

(w - c) - b in A

hence
w - c in A (-) B
; :: thesis: verum(w - c) - b in A

let b be Element of E; :: thesis: ( b in B implies (w - c) - b in A )

assume A6: b in B ; :: thesis: (w - c) - b in A

b + c in B (+) C by A5, A6;

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

hence (w - c) - b in A by RLVECT_1:27; :: thesis: verum

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

b + c in B (+) C by A5, A6;

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

hence (w - c) - b in A by RLVECT_1:27; :: thesis: verum