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

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