let S be non void Signature; :: thesis: for X being ManySortedSet of 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 ; :: 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 )
A0: dom X = the carrier of S by PARTFUN1:def 4;

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 Z0: X " {{} } c= rng the ResultSort of S by WMV;
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 A0, FUNCT_1:def 13;
then consider o being set such that
Z1: ( o in the carrier' of S & the ResultSort of S . o = s ) by Z0, FUNCT_2:17;
reconsider o = o as OperSymbol of S by Z1;
take o = o; :: thesis: the_result_sort_of o = s
thus the_result_sort_of o = s by Z1; :: thesis: verum

end;

assume Z2: 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 set ; :: according to TARSKI:def 3,ABCMIZ_1:def 55 :: thesis: ( not x in X " {{} } or x in rng the ResultSort of S )
assume x in X " {{} } ; :: thesis: x in rng the ResultSort of S
then A1: ( x in dom X & X . x in {{} } ) by FUNCT_1:def 13;
then reconsider x = x as SortSymbol of S by A0;
X . x = {} by A1, TARSKI:def 1;
then ex o being OperSymbol of S st the_result_sort_of o = x by Z2;
hence x in rng the ResultSort of S by FUNCT_2:6; :: thesis: verum