let X be non empty set ; :: thesis: for f, g being Function of X,BOOLEAN st { x where x is Element of X : f . x = TRUE } = { x where x is Element of X : g . x = TRUE } holds
f = g
let f, g be Function of X,BOOLEAN; :: thesis: ( { x where x is Element of X : f . x = TRUE } = { x where x is Element of X : g . x = TRUE } implies f = g )
set F = { x where x is Element of X : f . x = TRUE } ;
set G = { x where x is Element of X : g . x = TRUE } ;
assume A1: { x where x is Element of X : f . x = TRUE } = { x where x is Element of X : g . x = TRUE } ; :: thesis: f = g
for p being object st p in X holds
f . p = g . p

proof

let p be object ; :: thesis: ( p in X implies f . p = g . p )
assume A2: p in X ; :: thesis: f . p = g . p

per cases ( p in { x where x is Element of X : f . x = TRUE } or not p in { x where x is Element of X : f . x = TRUE } ) ;

suppose A3: p in { x where x is Element of X : f . x = TRUE } ; :: thesis: f . p = g . p

then A4: ex x1 being Element of X st
( x1 = p & f . x1 = TRUE ) ;
ex x2 being Element of X st
( x2 = p & g . x2 = TRUE ) by A1, A3;
hence f . p = g . p by A4; :: thesis: verum

end;

suppose A5: not p in { x where x is Element of X : f . x = TRUE } ; :: thesis: f . p = g . p

A6: f . p = FALSE

proof

assume A7: f . p <> FALSE ; :: thesis: contradiction
f . p in BOOLEAN by A2, FUNCT_2:5;
then f . p = TRUE by A7, TARSKI:def 2;
hence contradiction by A2, A5; :: thesis: verum

end;

g . p = FALSE

proof

assume A8: g . p <> FALSE ; :: thesis: contradiction
g . p in BOOLEAN by A2, FUNCT_2:5;
then g . p = TRUE by A8, TARSKI:def 2;
hence contradiction by A1, A2, A5; :: thesis: verum

end;

hence f . p = g . p by A6; :: thesis: verum

end;

end;

end;

hence f = g by FUNCT_2:12; :: thesis: verum