let f be complex-valued Function; :: thesis: for r being Complex st r <> 0 holds
(r (#) f) " = f "

let r be Complex; :: thesis: ( r <> 0 implies (r (#) f) " = f " )
assume A1: r <> 0 ; :: thesis: (r (#) f) " = f "
now :: thesis: for c being object holds
( ( c in (r (#) f) " implies c in f " ) & ( c in f " implies c in (r (#) f) " ) )
let c be object ; :: thesis: ( ( c in (r (#) f) " implies c in f " ) & ( c in f " implies c in (r (#) f) " ) )
reconsider cc = c as object ;
thus ( c in (r (#) f) " implies c in f " ) :: thesis: ( c in f " implies c in (r (#) f) " )
proof
assume A2: c in (r (#) f) " ; :: thesis: c in f "
then A3: c in dom (r (#) f) by FUNCT_1:def 7;
(r (#) f) . c in by ;
then (r (#) f) . c = 0 by TARSKI:def 1;
then r * (f . cc) = 0 by ;
then f . c = 0 by A1;
then A4: f . c in by TARSKI:def 1;
c in dom f by ;
hence c in f " by ; :: thesis: verum
end;
assume A5: c in f " ; :: thesis: c in (r (#) f) "
then f . c in 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 ;
then c in dom (r (#) f) by VALUED_1:def 5;
then (r (#) f) . c = 0 by ;
then A8: (r (#) f) . c in by TARSKI:def 1;
c in dom (r (#) f) by ;
hence c in (r (#) f) " by ; :: thesis: verum
end;
hence (r (#) f) " = f " by TARSKI:2; :: thesis: verum