let f, g be Function of [:F₁(),F₂():],F₃(); :: thesis: ( ( for x, y being object st x in F₁() & y in F₂() holds
f . (x,y) = F₄(x,y) ) & ( for x, y being object st x in F₁() & y in F₂() holds
g . (x,y) = F₄(x,y) ) implies f = g )
assume that
A1: for x, y being object st x in F₁() & y in F₂() holds
f . (x,y) = F₄(x,y) and
A2: for x, y being object st x in F₁() & y in F₂() holds
g . (x,y) = F₄(x,y) ; :: thesis: f = g
for a, b being set st a in F₁() & b in F₂() holds
f . (a,b) = g . (a,b)

proof

let a, b be set ; :: thesis: ( a in F₁() & b in F₂() implies f . (a,b) = g . (a,b) )
assume A3: ( a in F₁() & b in F₂() ) ; :: thesis: f . (a,b) = g . (a,b)
f . (a,b) = F₄(a,b) by A1, A3
.= g . (a,b) by A2, A3 ;
hence f . (a,b) = g . (a,b) ; :: thesis: verum

end;

hence f = g by BINOP_1:1; :: thesis: verum