let f be complex-valued Function; :: thesis: for r being complex number st r <> 0 holds
(r (#) f) " {0 } = f " {0 }
let r be complex number ; :: thesis: ( r <> 0 implies (r (#) f) " {0 } = f " {0 } )
assume A1: r <> 0 ; :: thesis: (r (#) f) " {0 } = f " {0 }

now

let c be set ; :: thesis: ( ( c in (r (#) f) " {0 } implies c in f " {0 } ) & ( c in f " {0 } implies c in (r (#) f) " {0 } ) )
thus ( c in (r (#) f) " {0 } implies c in f " {0 } ) :: thesis: ( c in f " {0 } implies c in (r (#) f) " {0 } )

proof

assume A2: c in (r (#) f) " {0 } ; :: thesis: c in f " {0 }
then A3: c in dom (r (#) f) by FUNCT_1:def 13;
(r (#) f) . c in {0 } by A2, FUNCT_1:def 13;
then (r (#) f) . c = 0 by TARSKI:def 1;
then r * (f . c) = 0 by A3, VALUED_1:def 5;
then f . c = 0 by A1;
then A4: f . c in {0 } by TARSKI:def 1;
c in dom f by A3, VALUED_1:def 5;
hence c in f " {0 } by A4, FUNCT_1:def 13; :: thesis: verum

end;

assume A5: c in f " {0 } ; :: thesis: c in (r (#) f) " {0 }
then f . c in {0 } by FUNCT_1:def 13;
then f . c = 0 by TARSKI:def 1;
then A6: r * (f . c) = 0 ;
A7: c in dom f by A5, FUNCT_1:def 13;
then c in dom (r (#) f) by VALUED_1:def 5;
then (r (#) f) . c = 0 by A6, VALUED_1:def 5;
then A8: (r (#) f) . c in {0 } by TARSKI:def 1;
c in dom (r (#) f) by A7, VALUED_1:def 5;
hence c in (r (#) f) " {0 } by A8, FUNCT_1:def 13; :: thesis: verum

end;

hence (r (#) f) " {0 } = f " {0 } by TARSKI:2; :: thesis: verum