let C be non empty set ; :: thesis: for f being PartFunc of C,COMPLEX
for r being Element of COMPLEX st r <> 0 holds
(r (#) f) " {0 } = f " {0 }
let f be PartFunc of C,COMPLEX ; :: thesis: for r being Element of COMPLEX st r <> 0 holds
(r (#) f) " {0 } = f " {0 }
let r be Element of COMPLEX ; :: thesis: ( r <> 0 implies (r (#) f) " {0 } = f " {0 } )
assume A1: r <> 0 ; :: thesis: (r (#) f) " {0 } = f " {0 }

now

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

proof

assume c in (r (#) f) " {0c } ; :: thesis: c in f " {0c }
then ( c in dom (r (#) f) & (r (#) f) /. c in {0c } ) by PARTFUN2:44;
then ( c in dom (r (#) f) & (r (#) f) /. c = 0c ) by TARSKI:def 1;
then ( c in dom (r (#) f) & r * (f /. c) = 0c ) by Th7;
then ( c in dom f & f /. c = 0c ) by A1, Th7, XCMPLX_1:6;
then ( c in dom f & f /. c in {0c } ) by TARSKI:def 1;
hence c in f " {0c } by PARTFUN2:44; :: thesis: verum

end;

assume c in f " {0c } ; :: thesis: c in (r (#) f) " {0c }
then ( c in dom f & f /. c in {0c } ) by PARTFUN2:44;
then ( c in dom f & f /. c = 0c ) by TARSKI:def 1;
then ( c in dom (r (#) f) & r * (f /. c) = 0c ) by Th7;
then ( c in dom (r (#) f) & (r (#) f) /. c = 0c ) by Th7;
then ( c in dom (r (#) f) & (r (#) f) /. c in {0c } ) by TARSKI:def 1;
hence c in (r (#) f) " {0c } by PARTFUN2:44; :: thesis: verum

end;

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