defpred S1[ Element of Y, set ] means ( ( ex x being Element of Y st
( x in EqClass ($1,PA) & a . x = TRUE ) implies $2 = TRUE ) & ( ( for x being Element of Y holds
( not x in EqClass ($1,PA) or not a . x = TRUE ) ) implies $2 = FALSE ) );
A1: for e being Element of Y ex u being Element of BOOLEAN st S1[e,u]
proof
let e be Element of Y; :: thesis: ex u being Element of BOOLEAN st S1[e,u]
per cases ( ex x being Element of Y st
( x in EqClass (e,PA) & a . x = TRUE ) or for x being Element of Y holds
( not x in EqClass (e,PA) or not a . x = TRUE ) ) ;
suppose ex x being Element of Y st
( x in EqClass (e,PA) & a . x = TRUE ) ; :: thesis: ex u being Element of BOOLEAN st S1[e,u]
hence ex u being Element of BOOLEAN st S1[e,u] ; :: thesis: verum
end;
suppose for x being Element of Y holds
( not x in EqClass (e,PA) or not a . x = TRUE ) ; :: thesis: ex u being Element of BOOLEAN st S1[e,u]
hence ex u being Element of BOOLEAN st S1[e,u] ; :: thesis: verum
end;
end;
end;
consider f being Function of Y,BOOLEAN such that
A2: for e being Element of Y holds S1[e,f . e] from FUNCT_2:sch 3(A1);
 reconsider f = f as Function of Y,BOOLEAN ;
reconsider f = f as Function of Y,BOOLEAN ;
take f ; :: thesis: for y being Element of Y holds
( ( ex x being Element of Y st
( x in EqClass (y,PA) & a . x = TRUE ) implies f . y = TRUE ) & ( ( for x being Element of Y holds
( not x in EqClass (y,PA) or not a . x = TRUE ) ) implies f . y = FALSE ) )
thus for y being Element of Y holds
( ( ex x being Element of Y st
( x in EqClass (y,PA) & a . x = TRUE ) implies f . y = TRUE ) & ( ( for x being Element of Y holds
( not x in EqClass (y,PA) or not a . x = TRUE ) ) implies f . y = FALSE ) ) by A2; :: thesis: verum