let D be non empty set ; 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; for r, s being Real st r <> 0 holds
F " {(s / r)} = (r (#) F) " {s}
let r, s be Real; ( r <> 0 implies F " {(s / r)} = (r (#) F) " {s} )
assume A1:
r <> 0
; F " {(s / r)} = (r (#) F) " {s}
thus
F " {(s / r)} c= (r (#) F) " {s}
XBOOLE_0:def 10 (r (#) F) " {s} c= F " {(s / r)}
let x be object ; TARSKI:def 3 ( not x in (r (#) F) " {s} or x in F " {(s / r)} )
assume A4:
x in (r (#) F) " {s}
; 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; verum