let X be set ; :: thesis: for Y being complex-functions-membered set

for f being PartFunc of X,Y

for g, h being complex-valued Function holds (f <-> g) <-> h = f <-> (g + h)

let Y be complex-functions-membered set ; :: thesis: for f being PartFunc of X,Y

for g, h being complex-valued Function holds (f <-> g) <-> h = f <-> (g + h)

let f be PartFunc of X,Y; :: thesis: for g, h being complex-valued Function holds (f <-> g) <-> h = f <-> (g + h)

let g, h be complex-valued Function; :: thesis: (f <-> g) <-> h = f <-> (g + h)

set f1 = f <-> g;

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

A2: dom ((f <-> g) <-> h) = (dom (f <-> g)) /\ (dom h) by Th61;

( dom (f <-> g) = (dom f) /\ (dom g) & dom (f <-> (g + h)) = (dom f) /\ (dom (g + h)) ) by Th61;

hence A3: dom ((f <-> g) <-> h) = dom (f <-> (g + h)) by A2, A1, XBOOLE_1:16; :: according to FUNCT_1:def 11 :: thesis: for b_{1} being object holds

( not b_{1} in dom ((f <-> g) <-> h) or ((f <-> g) <-> h) . b_{1} = (f <-> (g + h)) . b_{1} )

let x be object ; :: thesis: ( not x in dom ((f <-> g) <-> h) or ((f <-> g) <-> h) . x = (f <-> (g + h)) . x )

assume A4: x in dom ((f <-> g) <-> h) ; :: thesis: ((f <-> g) <-> h) . x = (f <-> (g + h)) . x

then A5: x in dom (f <-> g) by A2, XBOOLE_0:def 4;

A6: x in dom (g + h) by A3, A4, XBOOLE_0:def 4;

thus ((f <-> g) <-> h) . x = ((f <-> g) . x) - (h . x) by A4, Th62

.= ((f . x) - (g . x)) - (h . x) by A5, Th62

.= (f . x) - ((g . x) + (h . x)) by Th15

.= (f . x) - ((g + h) . x) by A6, VALUED_1:def 1

.= (f <-> (g + h)) . x by A3, A4, Th62 ; :: thesis: verum

for f being PartFunc of X,Y

for g, h being complex-valued Function holds (f <-> g) <-> h = f <-> (g + h)

let Y be complex-functions-membered set ; :: thesis: for f being PartFunc of X,Y

for g, h being complex-valued Function holds (f <-> g) <-> h = f <-> (g + h)

let f be PartFunc of X,Y; :: thesis: for g, h being complex-valued Function holds (f <-> g) <-> h = f <-> (g + h)

let g, h be complex-valued Function; :: thesis: (f <-> g) <-> h = f <-> (g + h)

set f1 = f <-> g;

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

A2: dom ((f <-> g) <-> h) = (dom (f <-> g)) /\ (dom h) by Th61;

( dom (f <-> g) = (dom f) /\ (dom g) & dom (f <-> (g + h)) = (dom f) /\ (dom (g + h)) ) by Th61;

hence A3: dom ((f <-> g) <-> h) = dom (f <-> (g + h)) by A2, A1, XBOOLE_1:16; :: according to FUNCT_1:def 11 :: thesis: for b

( not b

let x be object ; :: thesis: ( not x in dom ((f <-> g) <-> h) or ((f <-> g) <-> h) . x = (f <-> (g + h)) . x )

assume A4: x in dom ((f <-> g) <-> h) ; :: thesis: ((f <-> g) <-> h) . x = (f <-> (g + h)) . x

then A5: x in dom (f <-> g) by A2, XBOOLE_0:def 4;

A6: x in dom (g + h) by A3, A4, XBOOLE_0:def 4;

thus ((f <-> g) <-> h) . x = ((f <-> g) . x) - (h . x) by A4, Th62

.= ((f . x) - (g . x)) - (h . x) by A5, Th62

.= (f . x) - ((g . x) + (h . x)) by Th15

.= (f . x) - ((g + h) . x) by A6, VALUED_1:def 1

.= (f <-> (g + h)) . x by A3, A4, Th62 ; :: thesis: verum