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 <> {} ) ;

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

then ex m being OperSymbol of C st
( the_result_sort_of m = s & the_arity_of m = {} ) by A1;
hence contradiction by A3, Th5; :: thesis: verum

end;

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

then root-tree [ the Element of X . s,s] in the Sorts of (Free (C,X)) . s by Th4;
hence contradiction by A3; :: 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 3; :: thesis: verum