not {} in rng (MSFuncs D,D) by PBOOLE:149;
then reconsider X = product (MSFuncs D,D) as non empty set by CARD_3:37;
X is MSFunctionSet of D,D

proof

thus D is_transformable_to D ; :: according to AUTALG_1:def 6 :: thesis: for x being set st x in X holds
x is ManySortedFunction of D,D
let x be set ; :: thesis: ( x in X implies x is ManySortedFunction of D,D )
assume x in X ; :: thesis: x is ManySortedFunction of D,D
hence x is ManySortedFunction of D,D by Th21; :: thesis: verum

end;

then reconsider X = X as MSFunctionSet of D,D ;
take X ; :: thesis: not X is empty
thus not X is empty ; :: thesis: verum