let X, X1 be set ; :: thesis: for Y, Y1 being complex-functions-membered set
for c1, c2 being complex number
for f being PartFunc of X,Y
for f1 being PartFunc of X1,Y1 st f1 = f [/] c1 holds
f1 [/] c2 = f [/] (c1 * c2)
let Y, Y1 be complex-functions-membered set ; :: thesis: for c1, c2 being complex number
for f being PartFunc of X,Y
for f1 being PartFunc of X1,Y1 st f1 = f [/] c1 holds
f1 [/] c2 = f [/] (c1 * c2)
let c1, c2 be complex number ; :: thesis: for f being PartFunc of X,Y
for f1 being PartFunc of X1,Y1 st f1 = f [/] c1 holds
f1 [/] c2 = f [/] (c1 * c2)
let f be PartFunc of X,Y; :: thesis: for f1 being PartFunc of X1,Y1 st f1 = f [/] c1 holds
f1 [/] c2 = f [/] (c1 * c2)
let f1 be PartFunc of X1,Y1; :: thesis: ( f1 = f [/] c1 implies f1 [/] c2 = f [/] (c1 * c2) )
assume A1: f1 = f [/] c1 ; :: thesis: f1 [/] c2 = f [/] (c1 * c2)
then A2: dom f1 = dom f by Def38;
A3: dom (f1 [/] c2) = dom f1 by Def38;
hence A4: dom (f1 [/] c2) = dom (f [/] (c1 * c2)) by A2, Def38; :: according to FUNCT_1:def 17 :: thesis: for b₁ being set holds
( not b₁ in dom (f1 [/] c2) or (f1 [/] c2) . b₁ = (f [/] (c1 * c2)) . b₁ )
let x be set ; :: thesis: ( not x in dom (f1 [/] c2) or (f1 [/] c2) . x = (f [/] (c1 * c2)) . x )
assume A5: x in dom (f1 [/] c2) ; :: thesis: (f1 [/] c2) . x = (f [/] (c1 * c2)) . x
hence (f1 [/] c2) . x = (f1 . x) (#) (c2 " ) by Def38
.= ((f . x) (#) (c1 " )) (#) (c2 " ) by A1, A3, A5, Def38
.= (f . x) (#) ((c1 " ) * (c2 " )) by Th12
.= (f . x) (#) ((c1 * c2) " ) by XCMPLX_1:205
.= (f [/] (c1 * c2)) . x by A5, A4, Def38 ;
:: thesis: verum