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 & ( for x being object st x in dom f holds
f . x 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 & ( for x being object st x in dom f holds
f . x 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 & ( for x being object st x in dom f holds
f . x is non-empty ) & f [#] c1 = f [#] c2 holds
c1 = c2
let f be PartFunc of X,Y; :: thesis: ( f <> {} & f is non-empty & ( for x being object st x in dom f holds
f . x is non-empty ) & f [#] c1 = f [#] c2 implies c1 = c2 )
assume that
A1: f <> {} and
A2: f is non-empty and
A3: for x being object st x in dom f holds
f . x is non-empty and
A4: f [#] c1 = f [#] c2 ; :: thesis: c1 = c2
consider x being object such that
A5: x in dom f by A1, XBOOLE_0:def 1;
dom f = dom (f [#] c2) by Def39;
then A6: (f [#] c2) . x = (f . x) (#) c2 by A5, Def39;
dom f = dom (f [#] c1) by Def39;
then A7: (f [#] c1) . x = (f . x) (#) c1 by A5, Def39;
f . x in rng f by A5, FUNCT_1:def 3;
then A8: f . x <> {} by A2, RELAT_1:def 9;
f . x is non-empty by A3, A5;
hence c1 = c2 by A4, A8, A7, A6, Th9; :: thesis: verum