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

hence Free (C,X) is non-empty by MSUALG_1:def 3; :: thesis: verum

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))

then
the Sorts of (Free (C,X)) is V8()
by RELAT_1:def 9;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;

end;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;

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;( the_result_sort_of m = s & the_arity_of m = {} ) by A1;

hence contradiction by A3, Th5; :: thesis: verum

hence Free (C,X) is non-empty by MSUALG_1:def 3; :: thesis: verum