let c be Complex; :: thesis: for f, g being complex-valued Function holds (f (/) c) - (g (/) c) = (f - g) (/) c
let f, g be complex-valued Function; :: thesis: (f (/) c) - (g (/) c) = (f - g) (/) c
thus (f (/) c) - (g (/) c) = (f (/) c) + ((- g) (/) c) by VALUED_2:30
.= (f - g) (/) c by Th4 ; :: thesis: verum