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

A1: dom ((f (/) c) + (g (/) c)) = (dom (f (/) c)) /\ (dom (g (/) c)) by VALUED_1:def 1;

A2: dom (f (/) c) = dom f by VALUED_2:28;

A3: dom (g (/) c) = dom g by VALUED_2:28;

A4: dom ((f + g) (/) c) = dom (f + g) by VALUED_2:28;

A5: dom (f + g) = (dom f) /\ (dom g) by VALUED_1:def 1;

thus dom ((f (/) c) + (g (/) c)) = dom ((f + g) (/) c) by A1, A2, A3, A4, VALUED_1:def 1; :: according to FUNCT_1:def 11 :: thesis: for b_{1} being object holds

( not b_{1} in dom ((f (/) c) + (g (/) c)) or ((f (/) c) + (g (/) c)) . b_{1} = ((f + g) (/) c) . b_{1} )

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

assume A6: x in dom ((f (/) c) + (g (/) c)) ; :: thesis: ((f (/) c) + (g (/) c)) . x = ((f + g) (/) c) . x

thus ((f + g) (/) c) . x = ((f + g) . x) / c by VALUED_2:29

.= ((f . x) + (g . x)) / c by A1, A2, A3, A6, A5, VALUED_1:def 1

.= ((f . x) / c) + ((g . x) / c)

.= ((f . x) / c) + ((g (/) c) . x) by VALUED_2:29

.= ((f (/) c) . x) + ((g (/) c) . x) by VALUED_2:29

.= ((f (/) c) + (g (/) c)) . x by A6, VALUED_1:def 1 ; :: thesis: verum

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

A1: dom ((f (/) c) + (g (/) c)) = (dom (f (/) c)) /\ (dom (g (/) c)) by VALUED_1:def 1;

A2: dom (f (/) c) = dom f by VALUED_2:28;

A3: dom (g (/) c) = dom g by VALUED_2:28;

A4: dom ((f + g) (/) c) = dom (f + g) by VALUED_2:28;

A5: dom (f + g) = (dom f) /\ (dom g) by VALUED_1:def 1;

thus dom ((f (/) c) + (g (/) c)) = dom ((f + g) (/) c) by A1, A2, A3, A4, VALUED_1:def 1; :: according to FUNCT_1:def 11 :: thesis: for b

( not b

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

assume A6: x in dom ((f (/) c) + (g (/) c)) ; :: thesis: ((f (/) c) + (g (/) c)) . x = ((f + g) (/) c) . x

thus ((f + g) (/) c) . x = ((f + g) . x) / c by VALUED_2:29

.= ((f . x) + (g . x)) / c by A1, A2, A3, A6, A5, VALUED_1:def 1

.= ((f . x) / c) + ((g . x) / c)

.= ((f . x) / c) + ((g (/) c) . x) by VALUED_2:29

.= ((f (/) c) . x) + ((g (/) c) . x) by VALUED_2:29

.= ((f (/) c) + (g (/) c)) . x by A6, VALUED_1:def 1 ; :: thesis: verum