consider i being set such that
A1: ( i in the carrier of S & 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 & dom the Sorts of A = the carrier of S ) by A1, PARTFUN1:def 4;
hence not Union the Sorts of A is empty by A1, CARD_5:10; :: thesis: verum