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 A1: ( rng f1 c= Funcs X,Y & rng f2 c= Funcs X,Y & X <> {} & uncurry f1 = uncurry f2 ) ; :: thesis: f1 = f2
then A2: ( dom (uncurry f1) = [:(dom f1),X:] & dom (uncurry f2) = [:(dom f2),X:] ) by Th33;
( dom f1 = {} implies dom f1 = dom f2 ) by A1, A2, ZFMISC_1:113;
then A4: dom f1 = dom f2 by A1, A2, ZFMISC_1:134;

now

let x be set ; :: thesis: ( x in dom f1 implies f1 . x = f2 . x )
assume A5: x in dom f1 ; :: thesis: f1 . x = f2 . x
then A6: ( f1 . x in rng f1 & f2 . x in rng f2 ) by A4, FUNCT_1:def 5;
then consider g1 being Function such that
A7: ( f1 . x = g1 & dom g1 = X & rng g1 c= Y ) by A1, FUNCT_2:def 2;
consider g2 being Function such that
A8: ( f2 . x = g2 & dom g2 = X & rng g2 c= Y ) by A1, A6, FUNCT_2:def 2;

now

let y be set ; :: thesis: ( y in X implies g1 . y = g2 . y )
assume y in X ; :: thesis: g1 . y = g2 . y
then ( [x,y] in dom (uncurry f1) & [x,y] in dom (uncurry f2) & [x,y] `1 = x & [x,y] `2 = y ) by A1, A5, A7, Def4, MCART_1:7;
then ( (uncurry f1) . [x,y] = g1 . y & (uncurry f2) . [x,y] = g2 . y ) by A7, A8, Def4;
hence g1 . y = g2 . y by A1; :: thesis: verum

end;

hence f1 . x = f2 . x by A7, A8, FUNCT_1:9; :: thesis: verum

end;

hence f1 = f2 by A4, FUNCT_1:9; :: thesis: verum