let f, g be Function of [:F₁(),F₂():],BOOLEAN; :: thesis: ( ( for x, y being object st x in F₁() & y in F₂() holds
( ( P₁[x,y] implies f . (x,y) = TRUE ) & ( P₁[x,y] implies f . (x,y) = FALSE ) ) ) & ( for x, y being object st x in F₁() & y in F₂() holds
( ( P₁[x,y] implies g . (x,y) = TRUE ) & ( P₁[x,y] implies g . (x,y) = FALSE ) ) ) implies f = g )
assume that
A1: for x, y being object st x in F₁() & y in F₂() holds
( ( P₁[x,y] implies f . (x,y) = TRUE ) & ( P₁[x,y] implies f . (x,y) = FALSE ) ) and
A2: for x, y being object st x in F₁() & y in F₂() holds
( ( P₁[x,y] implies g . (x,y) = TRUE ) & ( P₁[x,y] implies g . (x,y) = FALSE ) ) ; :: 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) = g . (a,b)

proof

per cases ( P₁[a,b] or not P₁[a,b] ) ;

suppose A4: P₁[a,b] ; :: thesis: f . (a,b) = g . (a,b)

hence f . (a,b) = TRUE by A1, A3
.= g . (a,b) by A2, A3, A4 ;
:: thesis: verum

end;

suppose A5: P₁[a,b] ; :: thesis: f . (a,b) = g . (a,b)

hence f . (a,b) = FALSE by A1, A3
.= g . (a,b) by A2, A3, A5 ;
:: thesis: verum

end;

end;

end;

hence f . (a,b) = g . (a,b) ; :: thesis: verum

end;

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