let Y be non empty set ; :: thesis: for a being constant Element of Funcs Y,BOOLEAN holds
( a = O_el Y or a = I_el Y )
let a be constant Element of Funcs Y,BOOLEAN ; :: thesis: ( a = O_el Y or a = I_el Y )
consider f being Function such that
A1: ( a = f & dom f = Y & rng f c= BOOLEAN ) by FUNCT_2:def 2;
( ex n1, n2 being set st
( n1 in Y & n2 in Y & not a . n1 = a . n2 ) or for x being Element of Y holds a . x = TRUE or for x being Element of Y holds a . x = FALSE )

proof

assume A2: for n1, n2 being set st n1 in Y & n2 in Y holds
a . n1 = a . n2 ; :: thesis: ( for x being Element of Y holds a . x = TRUE or for x being Element of Y holds a . x = FALSE )

now

assume A3: ( not for x being Element of Y holds a . x = TRUE & not for x being Element of Y holds a . x = FALSE ) ; :: thesis: contradiction
then consider x1 being Element of Y such that
A4: a . x1 <> TRUE ;
consider x2 being Element of Y such that
A5: a . x2 <> FALSE by A3;
a . x1 = FALSE by A4, XBOOLEAN:def 3;
hence contradiction by A2, A5; :: thesis: verum

end;

hence ( for x being Element of Y holds a . x = TRUE or for x being Element of Y holds a . x = FALSE ) ; :: thesis: verum

end;

hence ( a = O_el Y or a = I_el Y ) by A1, Def13, Def14, FUNCT_1:def 16; :: thesis: verum