A1: dom the Sorts of A = the carrier of S by PARTFUN1:def 2;
consider i being object such that
A2: i in the carrier of S and
A3: not the Sorts of A . i is empty by PBOOLE:def 12;
set x = the Element of the Sorts of A . i;
the Element of the Sorts of A . i in the Sorts of A . i by A3;
hence not Union the Sorts of A is empty by A2, A1, CARD_5:2; :: thesis: verum