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, Th33; :: thesis: verum

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, Th33; :: thesis: verum