defpred S₁[ 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 S₁[e,u]

proof

let e be Element of Y; :: thesis: ex u being Element of BOOLEAN st S₁[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 S₁[e,u]

hence ex u being Element of BOOLEAN st S₁[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 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:11;
reconsider f = f as Element of Funcs 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