let D be non empty set ; :: thesis: for F being PartFunc of D, REAL
for r, s being real number st r <> 0 holds
F " {(s / r)} = (r (#) F) " {s}
let F be PartFunc of D, REAL ; :: thesis: for r, s being real number st r <> 0 holds
F " {(s / r)} = (r (#) F) " {s}
let r, s be real number ; :: 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 set ; :: 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 & F . d in {(s / r)} ) by A2, FUNCT_1:def 13;
then A3: ( d in dom (r (#) F) & F . d = s / r ) by TARSKI:def 1, VALUED_1:def 5;
then r * (F . d) = s by A1, XCMPLX_1:88;
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 13; :: thesis: verum

end;

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