let c be complex number ; :: thesis: for g, h being complex-valued Function holds (g + h) (/) c = (g (/) c) + (h (/) c)
let g, h be complex-valued Function; :: thesis: (g + h) (/) c = (g (/) c) + (h (/) c)
A3: dom (g (/) c) = dom g by VALUED_1:def 5;
A4: dom (h (/) c) = dom h by VALUED_1:def 5;
A2: dom ((g + h) (/) c) = dom (g + h) by VALUED_1:def 5;
dom (g + h) = (dom g) /\ (dom h) by VALUED_1:def 1;
hence A6: dom ((g + h) (/) c) = dom ((g (/) c) + (h (/) c)) by A3, A4, A2, VALUED_1:def 1; :: according to FUNCT_1:def 17 :: thesis: for b₁ being set holds
( not b₁ in dom ((g + h) (/) c) or ((g + h) (/) c) . b₁ = ((g (/) c) + (h (/) c)) . b₁ )
let x be set ; :: thesis: ( not x in dom ((g + h) (/) c) or ((g + h) (/) c) . x = ((g (/) c) + (h (/) c)) . x )
assume A5: x in dom ((g + h) (/) c) ; :: thesis: ((g + h) (/) c) . x = ((g (/) c) + (h (/) c)) . x
thus ((g + h) (/) c) . x = ((g + h) . x) * (c " ) by VALUED_1:6
.= ((g . x) + (h . x)) * (c " ) by A2, A5, VALUED_1:def 1
.= ((g . x) * (c " )) + ((h . x) * (c " ))
.= ((g (/) c) . x) + ((h . x) * (c " )) by VALUED_1:6
.= ((g (/) c) . x) + ((h (/) c) . x) by VALUED_1:6
.= ((g (/) c) + (h (/) c)) . x by A5, A6, VALUED_1:def 1 ; :: thesis: verum