begin
begin
begin
begin
definition
let Y be non
empty set ;
let a be
Function of
Y,
BOOLEAN;
let PA be
a_partition of
Y;
existence
ex b1 being Function of Y,BOOLEAN st
for y being Element of Y holds
( ( ( for x being Element of Y st x in EqClass (y,PA) holds
a . x = TRUE ) implies b1 . y = TRUE ) & ( ex x being Element of Y st
( x in EqClass (y,PA) & not a . x = TRUE ) implies b1 . y = FALSE ) )
uniqueness
for b1, b2 being Function of Y,BOOLEAN st ( for y being Element of Y holds
( ( ( for x being Element of Y st x in EqClass (y,PA) holds
a . x = TRUE ) implies b1 . y = TRUE ) & ( ex x being Element of Y st
( x in EqClass (y,PA) & not a . x = TRUE ) implies b1 . y = FALSE ) ) ) & ( for y being Element of Y holds
( ( ( for x being Element of Y st x in EqClass (y,PA) holds
a . x = TRUE ) implies b2 . y = TRUE ) & ( ex x being Element of Y st
( x in EqClass (y,PA) & not a . x = TRUE ) implies b2 . y = FALSE ) ) ) holds
b1 = b2
end;
definition
let Y be non
empty set ;
let a be
Function of
Y,
BOOLEAN;
let PA be
a_partition of
Y;
existence
ex b1 being Function of Y,BOOLEAN st
for y being Element of Y holds
( ( ex x being Element of Y st
( x in EqClass (y,PA) & a . x = TRUE ) implies b1 . y = TRUE ) & ( ( for x being Element of Y holds
( not x in EqClass (y,PA) or not a . x = TRUE ) ) implies b1 . y = FALSE ) )
uniqueness
for b1, b2 being Function of Y,BOOLEAN st ( for y being Element of Y holds
( ( ex x being Element of Y st
( x in EqClass (y,PA) & a . x = TRUE ) implies b1 . y = TRUE ) & ( ( for x being Element of Y holds
( not x in EqClass (y,PA) or not a . x = TRUE ) ) implies b1 . y = FALSE ) ) ) & ( for y being Element of Y holds
( ( ex x being Element of Y st
( x in EqClass (y,PA) & a . x = TRUE ) implies b2 . y = TRUE ) & ( ( for x being Element of Y holds
( not x in EqClass (y,PA) or not a . x = TRUE ) ) implies b2 . y = FALSE ) ) ) holds
b1 = b2
end;
begin