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 ;
dom f = dom (f [/] c2) by Def39;
then A6: (f [/] c2) . x = (f . x) (/) c2 by ;
dom f = dom (f [/] c1) by Def39;
then A7: (f [/] c1) . x = (f . x) (/) c1 by ;
f . x in rng f by ;
then A8: f . x <> {} by ;
f . x is non-empty by A3, A5;
hence c1 = c2 by A4, A8, A7, A6, Th33; :: thesis: verum