let C be non void Signature; :: thesis: for X being ManySortedSet of the carrier of C st ( for s being SortSymbol of C st X . s = {} holds
ex o being OperSymbol of C st
( the_result_sort_of o = s & the_arity_of o = {} ) ) holds
Free (C,X) is non-empty

let X be ManySortedSet of the carrier of C; :: thesis: ( ( for s being SortSymbol of C st X . s = {} holds
ex o being OperSymbol of C st
( the_result_sort_of o = s & the_arity_of o = {} ) ) implies Free (C,X) is non-empty )

assume A1: for s being SortSymbol of C st X . s = {} holds
ex o being OperSymbol of C st
( the_result_sort_of o = s & the_arity_of o = {} ) ; :: thesis: Free (C,X) is non-empty
now :: thesis: not {} in rng the Sorts of (Free (C,X))
assume {} in rng the Sorts of (Free (C,X)) ; :: thesis: contradiction
then consider s being object such that
A2: s in dom the Sorts of (Free (C,X)) and
A3: {} = the Sorts of (Free (C,X)) . s by FUNCT_1:def 3;
reconsider s = s as SortSymbol of C by A2;
set x = the Element of X . s;
per cases ( X . s = {} or X . s <> {} ) ;
end;
end;
then the Sorts of (Free (C,X)) is V8() by RELAT_1:def 9;
hence Free (C,X) is non-empty by MSUALG_1:def 3; :: thesis: verum