let f be complex-valued Function; :: thesis: for r being complex number holds abs (r (#) f) = (abs r) (#) (abs f)
let r be complex number ; :: thesis: abs (r (#) f) = (abs r) (#) (abs f)
A1: dom (abs (r (#) f)) = dom (r (#) f) by VALUED_1:def 11
.= dom f by VALUED_1:def 5
.= dom (abs f) by VALUED_1:def 11
.= dom ((abs r) (#) (abs f)) by VALUED_1:def 5 ;

now

let c be set ; :: thesis: ( c in dom (abs (r (#) f)) implies (abs (r (#) f)) . c = ((abs r) (#) (abs f)) . c )
assume A2: c in dom (abs (r (#) f)) ; :: thesis: (abs (r (#) f)) . c = ((abs r) (#) (abs f)) . c
then A3: c in dom (r (#) f) by VALUED_1:def 11;
thus (abs (r (#) f)) . c = abs ((r (#) f) . c) by VALUED_1:18
.= abs (r * (f . c)) by A3, VALUED_1:def 5
.= (abs r) * (abs (f . c)) by COMPLEX1:65
.= (abs r) * ((abs f) . c) by VALUED_1:18
.= ((abs r) (#) (abs f)) . c by A1, A2, VALUED_1:def 5 ; :: thesis: verum

end;

hence abs (r (#) f) = (abs r) (#) (abs f) by A1, FUNCT_1:2; :: thesis: verum