MSFuncs (A,B) is non-empty by A1, Th23;
then not {} in rng (MSFuncs (A,B)) by PBOOLE:137;
then reconsider X = product (MSFuncs (A,B)) as non empty set by CARD_3:26;
take X ; :: thesis: for x being set st x in X holds
x is ManySortedFunction of A,B
let x be set ; :: thesis: ( x in X implies x is ManySortedFunction of A,B )
assume x in X ; :: thesis: x is ManySortedFunction of A,B
hence x is ManySortedFunction of A,B by A1, Th21; :: thesis: verum