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 ) )

hence
arity (TrivialOp k) = k
by MARGREL1:def 25; :: thesis: verumlen 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;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