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 set ; :: 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 & F . d in {(s + r)} ) by A1, FUNCT_1:def 13;
then A3: ( d in dom (F - r) & F . d = s + r ) by TARSKI:def 1, VALUED_1:3;
then (F . d) - r = s ;
then (F - r) . d = s by A2, VALUED_1:3;
then (F - r) . d in {s} by TARSKI:def 1;
hence x in (F - r) " {s} by A3, FUNCT_1:def 13; :: thesis: verum

end;

let x be set ; :: 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) & (F - r) . d in {s} ) by A4, FUNCT_1:def 13;
then A5: ( d in dom F & (F - r) . d = s ) by TARSKI:def 1, VALUED_1:3;
then (F . d) - r = s by VALUED_1:3;
then F . d in {(s + r)} by TARSKI:def 1;
hence x in F " {(s + r)} by A5, FUNCT_1:def 13; :: thesis: verum