let X, Y be set ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 :: thesis: for x being object st x in dom f1 holds
f1 . x = f2 . x

let x be object ; :: thesis: ( x in dom f1 implies f1 . x = f2 . x )
assume A7: x in dom f1 ; :: thesis: f1 . x = f2 . x
then 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 :: thesis: for y being object st y in X holds
g1 . y = g2 . y

let y be object ; :: thesis: ( y in X implies g1 . y = g2 . y )
A12: ( [x,y] `1 = x & [x,y] `2 = y ) ;
assume A13: y in X ; :: thesis: g1 . y = g2 . y
then 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; :: thesis: verum

end;

hence f1 . x = f2 . x by A8, A9, A10, A11, FUNCT_1:2; :: thesis: verum

end;

hence f1 = f2 by A6; :: thesis: verum