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 A2: c in (r (#) f) " {0c } ; :: thesis: c in f " {0c }
then A3: c in dom (r (#) f) by PARTFUN2:44;
(r (#) f) /. c in {0c } by A2, PARTFUN2:44;
then (r (#) f) /. c = 0c by TARSKI:def 1;
then r * (f /. c) = 0c by A3, Th7;
then f /. c = 0c by A1, XCMPLX_1:6;
then A4: f /. c in {0c } by TARSKI:def 1;
c in dom f by A3, Th7;
hence c in f " {0c } by A4, PARTFUN2:44; :: thesis: verum

end;

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

end;

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