let X be set ; :: thesis: for Y being complex-functions-membered set
for c1, c2 being Complex
for f being PartFunc of X,Y st f <> {} & f is non-empty & f [+] c1 = f [+] c2 holds
c1 = c2
let Y be complex-functions-membered set ; :: thesis: for c1, c2 being Complex
for f being PartFunc of X,Y st f <> {} & f is non-empty & f [+] c1 = f [+] c2 holds
c1 = c2
let c1, c2 be Complex; :: thesis: for f being PartFunc of X,Y st f <> {} & f is non-empty & f [+] c1 = f [+] c2 holds
c1 = c2
let f be PartFunc of X,Y; :: thesis: ( f <> {} & f is non-empty & f [+] c1 = f [+] c2 implies c1 = c2 )
assume that
A1: f <> {} and
A2: f is non-empty and
A3: f [+] c1 = f [+] c2 ; :: thesis: c1 = c2
consider x being object such that
A4: x in dom f by A1, XBOOLE_0:def 1;
f . x in rng f by A4, FUNCT_1:def 3;
then A5: f . x <> {} by A2, RELAT_1:def 9;
dom f = dom (f [+] c2) by Def37;
then A6: (f [+] c2) . x = (f . x) + c2 by A4, Def37;
dom f = dom (f [+] c1) by Def37;
then (f [+] c1) . x = (f . x) + c1 by A4, Def37;
hence c1 = c2 by A3, A5, A6, Th7; :: thesis: verum