thus O_el Y is constant :: thesis: verum

proof

consider f being Function such that
A1: ( O_el Y = f & dom f = Y & rng f c= BOOLEAN ) by FUNCT_2:def 2;
for n1, n2 being set st n1 in dom (O_el Y) & n2 in dom (O_el Y) holds
(O_el Y) . n1 = (O_el Y) . n2

proof

let n1, n2 be set ; :: thesis: ( n1 in dom (O_el Y) & n2 in dom (O_el Y) implies (O_el Y) . n1 = (O_el Y) . n2 )
assume ( n1 in dom (O_el Y) & n2 in dom (O_el Y) ) ; :: thesis: (O_el Y) . n1 = (O_el Y) . n2
then reconsider n1 = n1, n2 = n2 as Element of Y by A1;
A2: (O_el Y) . n2 = FALSE by Def13;
(O_el Y) . n1 = (O_el Y) . n1 ;
hence (O_el Y) . n1 = (O_el Y) . n2 by A2, Def13; :: thesis: verum

end;

hence O_el Y is constant by FUNCT_1:def 16; :: thesis: verum

end;