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

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:44, FUNCT_1:def 2
.= |.(f . c).| by A2, FUNCT_1:def 2 ;
:: thesis: verum

end;

end;