defpred S₁[ Element of Y, set ] means ( ( ( for x being Element of Y st x in EqClass ($1,PA) holds
a . x = TRUE ) implies $2 = TRUE ) & ( ex x being Element of Y st
( x in EqClass ($1,PA) & not a . x = TRUE ) implies $2 = FALSE ) );
A1: for e being Element of Y ex u being Element of BOOLEAN st S₁[e,u]

proof

let e be Element of Y; :: thesis: ex u being Element of BOOLEAN st S₁[e,u]

per cases ( for x being Element of Y st x in EqClass (e,PA) holds
a . x = TRUE or ex x being Element of Y st
( x in EqClass (e,PA) & not a . x = TRUE ) ) ;

suppose for x being Element of Y st x in EqClass (e,PA) holds
a . x = TRUE ; :: thesis: ex u being Element of BOOLEAN st S₁[e,u]

hence ex u being Element of BOOLEAN st S₁[e,u] ; :: thesis: verum

end;

suppose ex x being Element of Y st
( x in EqClass (e,PA) & not a . x = TRUE ) ; :: thesis: ex u being Element of BOOLEAN st S₁[e,u]

hence ex u being Element of BOOLEAN st S₁[e,u] ; :: thesis: verum

end;

end;

end;

consider f being Function of Y,BOOLEAN such that
A2: for e being Element of Y holds S₁[e,f . e] from FUNCT_2:sch 3(A1);
reconsider f = f as Element of Funcs (Y,BOOLEAN) by FUNCT_2:8;
reconsider f = f as Element of Funcs (Y,BOOLEAN) ;
take f ; :: thesis: for y being Element of Y holds
( ( ( for x being Element of Y st x in EqClass (y,PA) holds
a . x = TRUE ) implies f . y = TRUE ) & ( ex x being Element of Y st
( x in EqClass (y,PA) & not a . x = TRUE ) implies f . y = FALSE ) )
thus for y being Element of Y holds
( ( ( for x being Element of Y st x in EqClass (y,PA) holds
a . x = TRUE ) implies f . y = TRUE ) & ( ex x being Element of Y st
( x in EqClass (y,PA) & not a . x = TRUE ) implies f . y = FALSE ) ) by A2; :: thesis: verum