let f be complex-valued Function; :: thesis: for c being set holds |.f.| . c = |.(f . c).|
A1: dom |.f.| = dom f by Def11;
let c be set ; :: thesis: |.f.| . c = |.(f . c).|

per cases ( c in dom f or not c in dom f ) ;

suppose c in dom f ; :: thesis: |.f.| . c = |.(f . c).|

hence |.f.| . c = |.(f . c).| by A1, Def11; :: thesis: verum

end;

suppose A2: not c in dom f ; :: thesis: |.f.| . c = |.(f . c).|

hence |.f.| . c = |.0 .| by A1, COMPLEX1:130, FUNCT_1:def 4
.= |.(f . c).| by A2, FUNCT_1:def 4 ;
:: thesis: verum

end;

end;