let f be complex-valued Function; :: thesis: for r being complex number st r <> 0 holds
(r (#) f) ^ = (r " ) (#) (f ^ )
let r be complex number ; :: thesis: ( r <> 0 implies (r (#) f) ^ = (r " ) (#) (f ^ ) )
assume A1: r <> 0 ; :: thesis: (r (#) f) ^ = (r " ) (#) (f ^ )
A2: dom ((r (#) f) ^ ) = (dom (r (#) f)) \ ((r (#) f) " {0 }) by Def8
.= (dom (r (#) f)) \ (f " {0 }) by A1, Th17
.= (dom f) \ (f " {0 }) by VALUED_1:def 5
.= dom (f ^ ) by Def8
.= dom ((r " ) (#) (f ^ )) by VALUED_1:def 5 ;

now

let c be set ; :: thesis: ( c in dom ((r (#) f) ^ ) implies ((r (#) f) ^ ) . c = ((r " ) (#) (f ^ )) . c )
assume A3: c in dom ((r (#) f) ^ ) ; :: thesis: ((r (#) f) ^ ) . c = ((r " ) (#) (f ^ )) . c
then A4: c in (dom (r (#) f)) \ ((r (#) f) " {0 }) by Def8;
A5: c in dom (f ^ ) by A2, A3, VALUED_1:def 5;
thus ((r (#) f) ^ ) . c = ((r (#) f) . c) " by A3, Def8
.= (r * (f . c)) " by A4, VALUED_1:def 5
.= (r " ) * ((f . c) " ) by XCMPLX_1:205
.= (r " ) * ((f ^ ) . c) by A5, Def8
.= ((r " ) (#) (f ^ )) . c by A2, A3, VALUED_1:def 5 ; :: thesis: verum

end;

hence (r (#) f) ^ = (r " ) (#) (f ^ ) by A2, FUNCT_1:9; :: thesis: verum