let S be non void Signature; :: thesis: for X being ManySortedSet of the carrier of S holds
( X is with_missing_variables iff for s being SortSymbol of S st X . s = {} holds
ex o being OperSymbol of S st the_result_sort_of o = s )
let X be ManySortedSet of the carrier of S; :: thesis: ( X is with_missing_variables iff for s being SortSymbol of S st X . s = {} holds
ex o being OperSymbol of S st the_result_sort_of o = s )
A1: dom X = the carrier of S by PARTFUN1:def 2;

hereby :: thesis: ( ( for s being SortSymbol of S st X . s = {} holds
ex o being OperSymbol of S st the_result_sort_of o = s ) implies X is with_missing_variables )

assume X is with_missing_variables ; :: thesis: for s being SortSymbol of S st X . s = {} holds
ex o being OperSymbol of S st the_result_sort_of o = s
then A2: X " {{}} c= rng the ResultSort of S ;
let s be SortSymbol of S; :: thesis: ( X . s = {} implies ex o being OperSymbol of S st the_result_sort_of o = s )
assume X . s = {} ; :: thesis: ex o being OperSymbol of S st the_result_sort_of o = s
then X . s in {{}} by TARSKI:def 1;
then s in X " {{}} by A1, FUNCT_1:def 7;
then consider o being object such that
A3: o in the carrier' of S and
A4: the ResultSort of S . o = s by A2, FUNCT_2:11;
reconsider o = o as OperSymbol of S by A3;
take o = o; :: thesis: the_result_sort_of o = s
thus the_result_sort_of o = s by A4; :: thesis: verum

end;

assume A5: for s being SortSymbol of S st X . s = {} holds
ex o being OperSymbol of S st the_result_sort_of o = s ; :: thesis: X is with_missing_variables
let x be object ; :: according to TARSKI:def 3,ABCMIZ_1:def 55 :: thesis: ( not x in X " {{}} or x in rng the ResultSort of S )
assume A6: x in X " {{}} ; :: thesis: x in rng the ResultSort of S
then A7: X . x in {{}} by FUNCT_1:def 7;
reconsider x = x as SortSymbol of S by A1, A6, FUNCT_1:def 7;
X . x = {} by A7, TARSKI:def 1;
then ex o being OperSymbol of S st the_result_sort_of o = x by A5;
hence x in rng the ResultSort of S by FUNCT_2:4; :: thesis: verum