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 ;

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

hence
abs (r (#) f) = |.r.| (#) (abs f)
by A1, FUNCT_1:2; :: thesis: verum(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;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