let X be set ; :: thesis: for Y being complex-functions-membered set
for c1, c2 being complex number
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 number
for f being PartFunc of X,Y holds (f [/] c1) [/] c2 = f [/] (c1 * c2)
let c1, c2 be complex number ; :: 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 17 :: thesis: for b₁ being set holds
( not b₁ in proj1 ((f [/] c1) [/] c2) or ((f [/] c1) [/] c2) . b₁ = (f [/] (c1 * c2)) . b₁ )
let x be set ; :: thesis: ( not x in proj1 ((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 . x) (#) ((c1 * c2) " ) by XCMPLX_1:205
.= (f [/] (c1 * c2)) . x by A2, A3, Def39 ;
:: thesis: verum