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 37;

A2: dom (f <-> ((dom f) --> c)) = (dom f) /\ (dom ((dom f) --> c)) by VALUED_2:61;

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 37;

A2: dom (f <-> ((dom f) --> c)) = (dom f) /\ (dom ((dom f) --> c)) by VALUED_2:61;

now :: thesis: for x being object st x in dom (f [-] c) holds

(f [-] c) . x = (f <-> ((dom f) --> c)) . x

hence
f [-] c = f <-> ((dom f) --> c)
by A1, A2; :: thesis: verum(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 = (f . x) - c by VALUED_2:def 37

.= (f . x) - (((dom f) --> c) . x) by A1, A4, FUNCOP_1:7

.= (f <-> ((dom f) --> c)) . x by A1, A2, A4, VALUED_2:62 ;

:: thesis: verum

end;assume A4: x in dom (f [-] c) ; :: thesis: (f [-] c) . x = (f <-> ((dom f) --> c)) . x

hence (f [-] c) . x = (f . x) - c by VALUED_2:def 37

.= (f . x) - (((dom f) --> c) . x) by A1, A4, FUNCOP_1:7

.= (f <-> ((dom f) --> c)) . x by A1, A2, A4, VALUED_2:62 ;

:: thesis: verum