let f be complex-valued Function; :: thesis: for r being Complex holds
( dom (f - r) = dom f & ( for c being object st c in dom f holds
(f - r) . c = (f . c) - r ) )
let r be Complex; :: thesis: ( dom (f - r) = dom f & ( for c being object st c in dom f holds
(f - r) . c = (f . c) - r ) )
dom (f - r) = dom f by Def2;
hence ( dom (f - r) = dom f & ( for c being object st c in dom f holds
(f - r) . c = (f . c) - r ) ) by Def2; :: thesis: verum