MSFuncs A,B is non-empty by A1, Th23;
then not {} in rng (MSFuncs A,B) by PBOOLE:149;
then reconsider X = product (MSFuncs A,B) as non empty set by CARD_3:37;
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