let f, g be Function of [:F1(),F2():],BOOLEAN; :: thesis: ( ( for x, y being object st x in F1() & y in F2() holds
( ( P1[x,y] implies f . (x,y) = TRUE ) & ( P1[x,y] implies f . (x,y) = FALSE ) ) ) & ( for x, y being object st x in F1() & y in F2() holds
( ( P1[x,y] implies g . (x,y) = TRUE ) & ( P1[x,y] implies g . (x,y) = FALSE ) ) ) implies f = g )
assume that
A1: for x, y being object st x in F1() & y in F2() holds
( ( P1[x,y] implies f . (x,y) = TRUE ) & ( P1[x,y] implies f . (x,y) = FALSE ) ) and
A2: for x, y being object st x in F1() & y in F2() holds
( ( P1[x,y] implies g . (x,y) = TRUE ) & ( P1[x,y] implies g . (x,y) = FALSE ) ) ; :: thesis: f = g
for a, b being set st a in F1() & b in F2() holds
f . (a,b) = g . (a,b)
proof
let a, b be set ; :: thesis: ( a in F1() & b in F2() implies f . (a,b) = g . (a,b) )
assume A3: ( a in F1() & b in F2() ) ; :: thesis: f . (a,b) = g . (a,b)
f . (a,b) = g . (a,b)
proof
per cases ( P1[a,b] or not P1[a,b] ) ;
suppose A4: P1[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: P1[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