let k be natural number ; :: thesis: arity (TrivialOp k) = k

now

dom (TrivialOp k) = {(k |-> {} )} by Def7;
then k |-> {} in dom (TrivialOp k) by TARSKI:def 1;
hence ex x being FinSequence st x in dom (TrivialOp k) ; :: thesis: for x being FinSequence st x in dom (TrivialOp k) holds
len x = k
let x be FinSequence; :: thesis: ( x in dom (TrivialOp k) implies len x = k )
assume x in dom (TrivialOp k) ; :: thesis: len x = k
then x in {(k |-> {} )} by Def7;
then x = k |-> {} by TARSKI:def 1;
hence len x = k by FINSEQ_1:def 18; :: thesis: verum

end;

hence arity (TrivialOp k) = k by MARGREL1:def 26; :: thesis: verum