let X be set ; for Y being complex-functions-membered set
for c1, c2 being Complex
for f being PartFunc of X,Y holds (f [/] c1) [/] c2 = f [/] (c1 * c2)
let Y be complex-functions-membered set ; for c1, c2 being Complex
for f being PartFunc of X,Y holds (f [/] c1) [/] c2 = f [/] (c1 * c2)
let c1, c2 be Complex; for f being PartFunc of X,Y holds (f [/] c1) [/] c2 = f [/] (c1 * c2)
let f be PartFunc of X,Y; (f [/] c1) [/] c2 = f [/] (c1 * c2)
set f1 = f [/] c1;
A1:
dom ((f [/] c1) [/] c2) = dom (f [/] c1)
by Def39;
dom (f [/] c1) = dom f
by Def39;
hence A2:
dom ((f [/] c1) [/] c2) = dom (f [/] (c1 * c2))
by A1, Def39; FUNCT_1:def 11 for b1 being object holds
( not b1 in dom ((f [/] c1) [/] c2) or ((f [/] c1) [/] c2) . b1 = (f [/] (c1 * c2)) . b1 )
let x be object ; ( not x in dom ((f [/] c1) [/] c2) or ((f [/] c1) [/] c2) . x = (f [/] (c1 * c2)) . x )
assume A3:
x in dom ((f [/] c1) [/] c2)
; ((f [/] c1) [/] c2) . x = (f [/] (c1 * c2)) . x
hence ((f [/] c1) [/] c2) . x =
((f [/] c1) . x) (#) (c2 ")
by Def39
.=
((f . x) (#) (c1 ")) (#) (c2 ")
by A1, A3, Def39
.=
(f . x) (#) ((c1 ") * (c2 "))
by Th16
.=
(f . x) (#) ((c1 * c2) ")
by XCMPLX_1:204
.=
(f [/] (c1 * c2)) . x
by A2, A3, Def39
;
verum