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 set st p in X holds
f . p = g . p

proof

let p be set ; :: 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 consider x1 being Element of X such that
A4: x1 = p and
A5: f . x1 = TRUE ;
consider x2 being Element of X such that
A6: x2 = p and
A7: g . x2 = TRUE by A1, A3;
thus f . p = g . p by A4, A5, A6, A7; :: thesis: verum

end;

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

A9: f . p = FALSE

proof

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

end;

g . p = FALSE

proof

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

end;

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

end;

end;

end;

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