let f1, f2 be complex-valued Function; :: thesis: abs (f1 (#) f2) = (abs f1) (#) (abs f2)

A1: now :: thesis: for c being object st c in dom (abs (f1 (#) f2)) holds
(abs (f1 (#) f2)) . c = ((abs f1) (#) (abs f2)) . c

let c be object ; :: thesis: ( c in dom (abs (f1 (#) f2)) implies (abs (f1 (#) f2)) . c = ((abs f1) (#) (abs f2)) . c )
assume c in dom (abs (f1 (#) f2)) ; :: thesis: (abs (f1 (#) f2)) . c = ((abs f1) (#) (abs f2)) . c
thus (abs (f1 (#) f2)) . c = |.((f1 (#) f2) . c).| by VALUED_1:18
.= |.((f1 . c) * (f2 . c)).| by VALUED_1:5
.= |.(f1 . c).| * |.(f2 . c).| by COMPLEX1:65
.= ((abs f1) . c) * |.(f2 . c).| by VALUED_1:18
.= ((abs f1) . c) * ((abs f2) . c) by VALUED_1:18
.= ((abs f1) (#) (abs f2)) . c by VALUED_1:5 ; :: thesis: verum

end;

dom (abs (f1 (#) f2)) = dom (f1 (#) f2) by VALUED_1:def 11
.= (dom f1) /\ (dom f2) by VALUED_1:def 4
.= (dom f1) /\ (dom (abs f2)) by VALUED_1:def 11
.= (dom (abs f1)) /\ (dom (abs f2)) by VALUED_1:def 11
.= dom ((abs f1) (#) (abs f2)) by VALUED_1:def 4 ;
hence abs (f1 (#) f2) = (abs f1) (#) (abs f2) by A1, FUNCT_1:2; :: thesis: verum