set n = 1;
take S = ManySortedSign(# {0},{1},({1} --> (In ((1 |-> 0),({0} *)))),({1} --> (In (0,{0}))) #); :: thesis: S is sufficiently_rich
let s be SortSymbol of S; :: according to MSAFREE5:def 4 :: thesis: ex o being OperSymbol of S st s in rng (the_arity_of o)
take o = In (1, the carrier' of S); :: thesis: 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; :: thesis: verum