let c be Complex; :: 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)

A1: dom ((g - h) (/) c) = dom (g - h) by VALUED_1:def 5;

A2: dom (g - h) = (dom g) /\ (dom h) by VALUED_1:12;

( dom (g (/) c) = dom g & dom (h (/) c) = dom h ) by VALUED_1:def 5;

hence A3: dom ((g - h) (/) c) = dom ((g (/) c) - (h (/) c)) by A1, A2, VALUED_1:12; :: according to FUNCT_1:def 11 :: thesis: for b_{1} being object holds

( not b_{1} in dom ((g - h) (/) c) or ((g - h) (/) c) . b_{1} = ((g (/) c) - (h (/) c)) . b_{1} )

let x be object ; :: thesis: ( not x in dom ((g - h) (/) c) or ((g - h) (/) c) . x = ((g (/) c) - (h (/) c)) . x )

assume A4: 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 A1, A4, VALUED_1:13

.= ((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 A3, A4, VALUED_1:13 ; :: thesis: verum

let g, h be complex-valued Function; :: thesis: (g - h) (/) c = (g (/) c) - (h (/) c)

A1: dom ((g - h) (/) c) = dom (g - h) by VALUED_1:def 5;

A2: dom (g - h) = (dom g) /\ (dom h) by VALUED_1:12;

( dom (g (/) c) = dom g & dom (h (/) c) = dom h ) by VALUED_1:def 5;

hence A3: dom ((g - h) (/) c) = dom ((g (/) c) - (h (/) c)) by A1, A2, VALUED_1:12; :: according to FUNCT_1:def 11 :: thesis: for b

( not b

let x be object ; :: thesis: ( not x in dom ((g - h) (/) c) or ((g - h) (/) c) . x = ((g (/) c) - (h (/) c)) . x )

assume A4: 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 A1, A4, VALUED_1:13

.= ((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 A3, A4, VALUED_1:13 ; :: thesis: verum