let f be complex-valued Function; :: 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}

(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 object holds

( ( c in (r (#) f) " {0} implies c in f " {0} ) & ( c in f " {0} implies c in (r (#) f) " {0} ) )

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

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

reconsider cc = c as object ;

thus ( c in (r (#) f) " {0} implies c in f " {0} ) :: thesis: ( c in f " {0} implies c in (r (#) f) " {0} )

then f . c in {0} by FUNCT_1:def 7;

then f . c = 0 by TARSKI:def 1;

then A6: r * (f . cc) = 0 ;

A7: c in dom f by A5, FUNCT_1:def 7;

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 7; :: thesis: verum

end;reconsider cc = c as object ;

thus ( c in (r (#) f) " {0} implies c in f " {0} ) :: thesis: ( c in f " {0} implies c in (r (#) f) " {0} )

proof

assume A5:
c in f " {0}
; :: thesis: c in (r (#) f) " {0}
assume A2:
c in (r (#) f) " {0}
; :: thesis: c in f " {0}

then A3: c in dom (r (#) f) by FUNCT_1:def 7;

(r (#) f) . c in {0} by A2, FUNCT_1:def 7;

then (r (#) f) . c = 0 by TARSKI:def 1;

then r * (f . cc) = 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 7; :: thesis: verum

end;then A3: c in dom (r (#) f) by FUNCT_1:def 7;

(r (#) f) . c in {0} by A2, FUNCT_1:def 7;

then (r (#) f) . c = 0 by TARSKI:def 1;

then r * (f . cc) = 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 7; :: thesis: verum

then f . c in {0} by FUNCT_1:def 7;

then f . c = 0 by TARSKI:def 1;

then A6: r * (f . cc) = 0 ;

A7: c in dom f by A5, FUNCT_1:def 7;

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 7; :: thesis: verum