let f be complex-valued Function; :: thesis: for r being Complex holds abs (r (#) f) = |.r.| (#) (abs f)
let r be Complex; :: thesis: abs (r (#) f) = |.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 (|.r.| (#) (abs f)) by VALUED_1:def 5 ;

now :: thesis: for c being object st c in dom (abs (r (#) f)) holds
(abs (r (#) f)) . c = (|.r.| (#) (abs f)) . c

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

end;

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