for n1, n2 being object 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 object ; :: 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 PARTFUN1:def 2;
( (O_el Y) . n2 = FALSE & (O_el Y) . n1 = (O_el Y) . n1 ) by Def10;
hence (O_el Y) . n1 = (O_el Y) . n2 by Def10; :: thesis: verum

end;

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