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) ^ = (r " ) (#) (f ^ )
let f be PartFunc of C,COMPLEX ; :: thesis: for r being Element of COMPLEX st r <> 0 holds
(r (#) f) ^ = (r " ) (#) (f ^ )
let r be Element of COMPLEX ; :: 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) " {0c }) by Def2
.= (dom (r (#) f)) \ (f " {0c }) by A1, Th21
.= (dom f) \ (f " {0c }) by Th7
.= dom (f ^ ) by Def2
.= dom ((r " ) (#) (f ^ )) by Th7 ;

now

let c be Element of C; :: 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 (f ^ ) by A2, Th7;
c in (dom (r (#) f)) \ ((r (#) f) " {0c }) by A3, Def2;
then A5: c in dom (r (#) f) by XBOOLE_0:def 5;
thus ((r (#) f) ^ ) /. c = ((r (#) f) /. c) " by A3, Def2
.= (r * (f /. c)) " by A5, Th7
.= (r " ) * ((f /. c) " ) by XCMPLX_1:205
.= (r " ) * ((f ^ ) /. c) by A4, Def2
.= ((r " ) (#) (f ^ )) /. c by A2, A3, Th7 ; :: thesis: verum

end;

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