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;
A2: dom (f <#> g) = (dom f) /\ (dom g) by Def42;
A3: dom ((f <#> g) <#> h) = (dom (f <#> g)) /\ (dom h) by Def42;
A4: dom (f <#> (g (#) h)) = (dom f) /\ (dom (g (#) h)) by Def42;
dom (g (#) h) = (dom g) /\ (dom h) by VALUED_1:def 4;
hence A5: dom ((f <#> g) <#> h) = dom (f <#> (g (#) h)) by A2, A3, A4, XBOOLE_1:16; :: according to FUNCT_1:def 17 :: thesis: for b₁ being set holds
( not b₁ in dom ((f <#> g) <#> h) or ((f <#> g) <#> h) . b₁ = (f <#> (g (#) h)) . b₁ )
let x be set ; :: thesis: ( not x in dom ((f <#> g) <#> h) or ((f <#> g) <#> h) . x = (f <#> (g (#) h)) . x )
assume A6: x in dom ((f <#> g) <#> h) ; :: thesis: ((f <#> g) <#> h) . x = (f <#> (g (#) h)) . x
then A7: x in dom (f <#> g) by A3, XBOOLE_0:def 4;
A8: x in dom (g (#) h) by A6, A5, XBOOLE_0:def 4;
thus ((f <#> g) <#> h) . x = ((f <#> g) . x) (#) (h . x) by A6, Def42
.= ((f . x) (#) (g . x)) (#) (h . x) by A7, Def42
.= (f . x) (#) ((g . x) * (h . x)) by Th12
.= (f . x) (#) ((g (#) h) . x) by A8, VALUED_1:def 4
.= (f <#> (g (#) h)) . x by A6, A5, Def42 ; :: thesis: verum