take S = ManySortedSign(# {0},{1},({1} --> (In ((n |-> 0),({0} *)))),({1} --> (In (0,{0}))) #); :: thesis: S is n -ary_oper_including
take o = In (1, the carrier' of S); :: according to MSAFREE5:def 6 :: thesis: len (the_arity_of o) = n
A2: ( o = 1 & In (0,{0}) = 0 ) by TARSKI:def 1;
A3: the_arity_of o = In ((n |-> 0),({0} *)) by FUNCOP_1:7;
n |-> (In (0,{0})) is FinSequence of {0} ;
then n |-> 0 in {0} * by A2, FINSEQ_1:def 11;
then the_arity_of o = n |-> 0 by A3, SUBSET_1:def 8;
hence len (the_arity_of o) = n by CARD_1:def 7; :: thesis: verum