thus I_el Y is constant :: thesis: verum

proof

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

proof

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

end;

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

end;