let f1, f2 be complex-valued Function; :: thesis: for c being object st c in dom (f1 - f2) holds
(f1 - f2) . c = (f1 . c) - (f2 . c)
let c be object ; :: thesis: ( c in dom (f1 - f2) implies (f1 - f2) . c = (f1 . c) - (f2 . c) )
assume c in dom (f1 - f2) ; :: thesis: (f1 - f2) . c = (f1 . c) - (f2 . c)
hence (f1 - f2) . c = (f1 . c) + ((- f2) . c) by Def1
.= (f1 . c) - (f2 . c) by Th8 ;
:: thesis: verum