thus O_el Y is constant :: thesis: verum

proof

A1: ex f being Function st
( 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;
( (O_el Y) . n2 = FALSE & (O_el Y) . n1 = (O_el Y) . n1 ) by Def13;
hence (O_el Y) . n1 = (O_el Y) . n2 by Def13; :: thesis: verum

end;

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

end;