let S be non void Signature; :: thesis: ( S is arity-rich implies S is with_an_operation_for_each_sort )
assume A1: for n being Nat
for s being SortSymbol of S holds { o where o is OperSymbol of S : ( the_result_sort_of o = s & len (the_arity_of o) = n ) } is infinite ; :: according to ABCMIZ_A:def 12 :: thesis: S is with_an_operation_for_each_sort
let v be object ; :: according to TARSKI:def 3,ABCMIZ_1:def 54 :: thesis: ( not v in the carrier of S or v in rng the ResultSort of S )
assume v in the carrier of S ; :: thesis: v in rng the ResultSort of S
then reconsider v = v as SortSymbol of S ;
set A = { o where o is OperSymbol of S : ( the_result_sort_of o = v & len (the_arity_of o) = 0 ) } ;
reconsider A = { o where o is OperSymbol of S : ( the_result_sort_of o = v & len (the_arity_of o) = 0 ) } as infinite set by A1;
set a = the Element of A;
the Element of A in A ;
then consider o being OperSymbol of S such that
A2: ( the Element of A = o & the_result_sort_of o = v & len (the_arity_of o) = 0 ) ;
thus v in rng the ResultSort of S by A2, FUNCT_2:4; :: thesis: verum