let X be set ; :: thesis: 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 ; :: thesis: for c1, c2 being Complex

for f being PartFunc of X,Y holds (f [#] c1) [#] c2 = f [#] (c1 * c2)

let c1, c2 be Complex; :: thesis: for f being PartFunc of X,Y holds (f [#] c1) [#] c2 = f [#] (c1 * c2)

let f be PartFunc of X,Y; :: thesis: (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; :: according to FUNCT_1:def 11 :: thesis: for b_{1} being object holds

( not b_{1} in dom ((f [#] c1) [#] c2) or ((f [#] c1) [#] c2) . b_{1} = (f [#] (c1 * c2)) . b_{1} )

let x be object ; :: thesis: ( not x in dom ((f [#] c1) [#] c2) or ((f [#] c1) [#] c2) . x = (f [#] (c1 * c2)) . x )

assume A3: x in dom ((f [#] c1) [#] c2) ; :: thesis: ((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 [#] (c1 * c2)) . x by A2, A3, Def39 ;

:: thesis: verum

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 ; :: thesis: for c1, c2 being Complex

for f being PartFunc of X,Y holds (f [#] c1) [#] c2 = f [#] (c1 * c2)

let c1, c2 be Complex; :: thesis: for f being PartFunc of X,Y holds (f [#] c1) [#] c2 = f [#] (c1 * c2)

let f be PartFunc of X,Y; :: thesis: (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; :: according to FUNCT_1:def 11 :: thesis: for b

( not b

let x be object ; :: thesis: ( not x in dom ((f [#] c1) [#] c2) or ((f [#] c1) [#] c2) . x = (f [#] (c1 * c2)) . x )

assume A3: x in dom ((f [#] c1) [#] c2) ; :: thesis: ((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 [#] (c1 * c2)) . x by A2, A3, Def39 ;

:: thesis: verum