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

now :: thesis: for c being Element of C holds
( ( c in (r (#) f) " {0c} implies c in f " {0c} ) & ( c in f " {0c} implies c in (r (#) f) " {0c} ) )

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

end;

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

end;

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