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 Def7;

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, Def7; :: thesis: verum

end;

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

hence (f ") . c = 0 " by A1, FUNCT_1:def 2
.= (f . c) " by A2, FUNCT_1:def 2 ;
:: thesis: verum

end;

end;