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