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

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