set n = 1;
take S = ManySortedSign(# {0},{1},({1} --> (In ((1 |-> 0),({0} *)))),({1} --> (In (0,{0}))) #); S is sufficiently_rich
let s be SortSymbol of S; MSAFREE5:def 4 ex o being OperSymbol of S st s in rng (the_arity_of o)
take o = In (1, the carrier' of S); s in rng (the_arity_of o)
A1:
( 1 in {1} & 0 in {0} & s = 0 )
by TARSKI:def 1;
A2:
( o = 1 & In (0,{0}) = 0 )
by TARSKI:def 1;
1 |-> (In (0,{0})) is FinSequence of {0}
;
then
1 |-> 0 in {0} *
by A2, FINSEQ_1:def 11;
then
( the_arity_of o = 1 |-> 0 & 1 |-> 0 = <*0*> )
by SUBSET_1:def 8, FINSEQ_2:59;
hence
s in rng (the_arity_of o)
by A1, FINSEQ_1:39; verum