let X be ManySortedSet of the carrier of C; :: thesis: X is with_missing_variables
A1: X " {{}} c= dom X by RELAT_1:132;
A2: dom X = the carrier of C by PARTFUN1:def 2;
the carrier of C c= rng the ResultSort of C by Def54;
hence X " {{}} c= rng the ResultSort of C by A1, A2; :: according to ABCMIZ_1:def 55 :: thesis: verum