let X be set ; :: thesis: for c being Complex
for Y being complex-functions-membered set
for f being PartFunc of X,Y holds f [#] c = f <#> ((dom f) --> c)
let c be Complex; :: thesis: for Y being complex-functions-membered set
for f being PartFunc of X,Y holds f [#] c = f <#> ((dom f) --> c)
let Y be complex-functions-membered set ; :: thesis: for f being PartFunc of X,Y holds f [#] c = f <#> ((dom f) --> c)
let f be PartFunc of X,Y; :: thesis: f [#] c = f <#> ((dom f) --> c)
set g = (dom f) --> c;
A1: dom (f [#] c) = dom f by VALUED_2:def 39;
A2: dom (f <#> ((dom f) --> c)) = (dom f) /\ (dom ((dom f) --> c)) by VALUED_2:def 43;

now :: thesis: for x being object st x in dom (f [#] c) holds
(f [#] c) . x = (f <#> ((dom f) --> c)) . x

let x be object ; :: thesis: ( x in dom (f [#] c) implies (f [#] c) . x = (f <#> ((dom f) --> c)) . x )
assume A4: x in dom (f [#] c) ; :: thesis: (f [#] c) . x = (f <#> ((dom f) --> c)) . x
hence (f [#] c) . x = c (#) (f . x) by VALUED_2:def 39
.= (f . x) (#) (((dom f) --> c) . x) by A1, A4, FUNCOP_1:7
.= (f <#> ((dom f) --> c)) . x by A1, A2, A4, VALUED_2:def 43 ;
:: thesis: verum

end;

hence f [#] c = f <#> ((dom f) --> c) by A1, A2; :: thesis: verum