let D be non empty set ; :: thesis: for F being PartFunc of D,REAL
for r, s being Real st r <> 0 holds
F " {(s / r)} = (r (#) F) " {s}
let F be PartFunc of D,REAL; :: thesis: for r, s being Real st r <> 0 holds
F " {(s / r)} = (r (#) F) " {s}
let r, s be Real; :: thesis: ( r <> 0 implies F " {(s / r)} = (r (#) F) " {s} )
assume A1: r <> 0 ; :: thesis: F " {(s / r)} = (r (#) F) " {s}
thus F " {(s / r)} c= (r (#) F) " {s} :: according to XBOOLE_0:def 10 :: thesis: (r (#) F) " {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 (r (#) F) " {s} )
assume A2: x in F " {(s / r)} ; :: thesis: x in (r (#) F) " {s}
then reconsider d = x as Element of D ;
d in dom F by A2, FUNCT_1:def 7;
then A3: d in dom (r (#) F) by VALUED_1:def 5;
F . d in {(s / r)} by A2, FUNCT_1:def 7;
then F . d = s / r by TARSKI:def 1;
then r * (F . d) = s by A1, XCMPLX_1:87;
then (r (#) F) . d = s by A3, VALUED_1:def 5;
then (r (#) F) . d in {s} by TARSKI:def 1;
hence x in (r (#) F) " {s} by A3, FUNCT_1:def 7; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (r (#) F) " {s} or x in F " {(s / r)} )
assume A4: x in (r (#) F) " {s} ; :: thesis: x in F " {(s / r)}
then reconsider d = x as Element of D ;
A5: d in dom (r (#) F) by A4, FUNCT_1:def 7;
(r (#) F) . d in {s} by A4, FUNCT_1:def 7;
then (r (#) F) . d = s by TARSKI:def 1;
then r * (F . d) = s by A5, VALUED_1:def 5;
then F . d = s / r by A1, XCMPLX_1:89;
then A6: F . d in {(s / r)} by TARSKI:def 1;
d in dom F by A5, VALUED_1:def 5;
hence x in F " {(s / r)} by A6, FUNCT_1:def 7; :: thesis: verum