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