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 <> {} & uncurry' f1 = uncurry' f2 ) ; :: thesis: f1 = f2
dom (uncurry f1) = [:(dom f1),X:] by A1, Th19;
then A4: uncurry f1 = ~ (~ (uncurry f1)) by FUNCT_4:52;
dom (uncurry f2) = [:(dom f2),X:] by A2, Th19;
hence f1 = f2 by A1, A2, A3, A4, Th39, FUNCT_4:52; :: thesis: verum