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) )

proof

let x be object ; :: thesis: ( x in (A (-) B) (-) C iff x in A (-) (B (+) C) )

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

assume 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 ) ) ;

now :: thesis: for bc being Element of E st bc in B (+) C holds
w - 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;

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

end;

assume x in A (-) (B (+) C) ; :: thesis: 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 ) ) ;

now :: thesis: for c being Element of E st c in C holds
w - 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

now :: thesis: for b being Element of E st b in B holds
(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;

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

end;

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

end;

hence (A (-) B) (-) C = A (-) (B (+) C) by TARSKI:2; :: thesis: verum