let C be non void Signature; :: thesis: for X being ManySortedSet of 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 ; :: 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

assume {} in rng the Sorts of (Free C,X) ; :: thesis: contradiction
then consider s being set such that
A2: ( s in dom the Sorts of (Free C,X) & {} = the Sorts of (Free C,X) . s ) by FUNCT_1:def 5;
reconsider s = s as SortSymbol of C by A2, PARTFUN1:def 4;
consider x being Element of X . s;

per cases ( X . s = {} or X . s <> {} ) ;

suppose X . s = {} ; :: thesis: contradiction

then consider m being OperSymbol of C such that
A3: ( the_result_sort_of m = s & the_arity_of m = {} ) by A1;
thus contradiction by A2, A3, Th6; :: thesis: verum

end;

suppose X . s <> {} ; :: thesis: contradiction

then root-tree [x,s] in the Sorts of (Free C,X) . s by Th5;
hence contradiction by A2; :: thesis: verum

end;

end;

end;

then the Sorts of (Free C,X) is non-empty by RELAT_1:def 9;
hence Free C,X is non-empty by MSUALG_1:def 8; :: thesis: verum