thus I_el Y is constant :: thesis: verum
proof
for n1, n2 being object 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 object ; :: 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 PARTFUN1:def 2;
( (I_el Y) . n2 = TRUE & (I_el Y) . n1 = (I_el Y) . n1 ) by Def11;
hence (I_el Y) . n1 = (I_el Y) . n2 by Def11; :: thesis: verum
end;
hence I_el Y is constant by FUNCT_1:def 10; :: thesis: verum
end;