let D be non empty set ; :: thesis: for F being PartFunc of D,REAL
for r, s being Real holds F " {(s + r)} = (F - r) " {s}
let F be PartFunc of D,REAL; :: thesis: for r, s being Real holds F " {(s + r)} = (F - r) " {s}
let r, s be Real; :: thesis: F " {(s + r)} = (F - r) " {s}
thus F " {(s + r)} c= (F - r) " {s} :: according to XBOOLE_0:def 10 :: thesis: (F - r) " {s} c= F " {(s + r)}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in F " {(s + r)} or x in (F - r) " {s} )
assume A1: x in F " {(s + r)} ; :: thesis: x in (F - r) " {s}
then reconsider d = x as Element of D ;
A2: d in dom F by A1, FUNCT_1:def 7;
F . d in {(s + r)} by A1, FUNCT_1:def 7;
then F . d = s + r by TARSKI:def 1;
then (F . d) - r = s ;
then (F - r) . d = s by A2, VALUED_1:3;
then A3: (F - r) . d in {s} by TARSKI:def 1;
d in dom (F - r) by A2, VALUED_1:3;
hence x in (F - r) " {s} by A3, FUNCT_1:def 7; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (F - r) " {s} or x in F " {(s + r)} )
assume A4: x in (F - r) " {s} ; :: thesis: x in F " {(s + r)}
then reconsider d = x as Element of D ;
d in dom (F - r) by A4, FUNCT_1:def 7;
then A5: d in dom F by VALUED_1:3;
(F - r) . d in {s} by A4, FUNCT_1:def 7;
then (F - r) . d = s by TARSKI:def 1;
then (F . d) - r = s by A5, VALUED_1:3;
then F . d in {(s + r)} by TARSKI:def 1;
hence x in F " {(s + r)} by A5, FUNCT_1:def 7; :: thesis: verum