let k be Nat; :: thesis: arity (TrivialOp k) = k

now :: thesis: ( ex x being FinSequence st x in dom (TrivialOp k) & ( for x being FinSequence st x in dom (TrivialOp k) holds
len x = k ) )

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 CARD_1:def 7; :: thesis: verum

end;

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