let X, Y be set ; for f1, f2 being Function st rng f1 c= Funcs (X,Y) & rng f2 c= Funcs (X,Y) & X <> {} & uncurry f1 = uncurry f2 holds
f1 = f2
let f1, f2 be Function; ( rng f1 c= Funcs (X,Y) & rng f2 c= Funcs (X,Y) & X <> {} & uncurry f1 = uncurry f2 implies f1 = f2 )
assume that
A1:
rng f1 c= Funcs (X,Y)
and
A2:
rng f2 c= Funcs (X,Y)
and
A3:
X <> {}
and
A4:
uncurry f1 = uncurry f2
; f1 = f2
A5:
( dom (uncurry f1) = [:(dom f1),X:] & dom (uncurry f2) = [:(dom f2),X:] )
by A1, A2, Th19;
then
( dom f1 = {} implies dom f1 = dom f2 )
by A3, A4;
then A6:
dom f1 = dom f2
by A3, A4, A5, ZFMISC_1:110;
now for x being object st x in dom f1 holds
f1 . x = f2 . xlet x be
object ;
( x in dom f1 implies f1 . x = f2 . x )assume A7:
x in dom f1
;
f1 . x = f2 . xthen
f1 . x in rng f1
by FUNCT_1:def 3;
then consider g1 being
Function such that A8:
f1 . x = g1
and A9:
dom g1 = X
and
rng g1 c= Y
by A1, FUNCT_2:def 2;
f2 . x in rng f2
by A6, A7, FUNCT_1:def 3;
then consider g2 being
Function such that A10:
f2 . x = g2
and A11:
dom g2 = X
and
rng g2 c= Y
by A2, FUNCT_2:def 2;
now for y being object st y in X holds
g1 . y = g2 . ylet y be
object ;
( y in X implies g1 . y = g2 . y )A12:
(
[x,y] `1 = x &
[x,y] `2 = y )
;
assume A13:
y in X
;
g1 . y = g2 . ythen A14:
[x,y] in dom (uncurry f2)
by A4, A7, A8, A9, Def2;
[x,y] in dom (uncurry f1)
by A7, A8, A9, A13, Def2;
then
(uncurry f1) . [x,y] = g1 . y
by A8, A12, Def2;
hence
g1 . y = g2 . y
by A4, A10, A14, A12, Def2;
verum end; hence
f1 . x = f2 . x
by A8, A9, A10, A11, FUNCT_1:2;
verum end;
hence
f1 = f2
by A6; verum