set G = UN;
A1: dom (disjoin x) = I by PARTFUN1:def 2;
A2: dom x = I by PARTFUN1:def 2;
reconsider domx = dom x as Element of UN ;
reconsider dx = disjoin x as I -defined Function ;
A3: rng (disjoin x) c= UN

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in rng (disjoin x) or o in UN )
assume o in rng (disjoin x) ; :: thesis: o in UN
then consider o9 being object such that
A4: o9 in dom dx and
A5: o = dx . o9 by FUNCT_1:def 3;
A6: UN is axiom_GU1 ;
A7: o9 in dom x by A4, CARD_3:def 3;
reconsider o9 = o9 as Element of UN by A6, A4;
A8: o = [:(x . o9),{o9}:] by A7, A5, CARD_3:def 3;

now :: thesis: ( x . o9 in UN & {o9} in UN )

x . o9 in rng x by A4, A2, FUNCT_1:def 3;
hence x . o9 in UN ; :: thesis: {o9} in UN
thus {o9} in UN ; :: thesis: verum

end;

then reconsider xo9 = x . o9, enso9 = {o9} as Element of UN ;
[:xo9,enso9:] is Element of UN ;
hence o in UN by A8; :: thesis: verum

end;

reconsider dx = disjoin x as Function of I,UN by A1, A3, FUNCT_2:2;
dx is UN -valued ManySortedSet of I ;
hence disjoin x is UN -valued ManySortedSet of I ; :: thesis: verum