let X be set ; 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 ; 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; 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; ( 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
; 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; verum