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

proof

let x be object ; :: thesis:

hereby :: thesis:

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

let bc be Element of E; :: thesis:
assume bc in B (+) C ; :: thesis:
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:

end;

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

end;

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

let c be Element of E; :: thesis:
assume A5: c in C ; :: thesis:

now :: thesis:

let b be Element of E; :: thesis:
assume A6: b in B ; :: thesis:
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:

end;

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

end;

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

end;

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