let k be Nat; :: thesis: for a being set holds len (k |-> a) = k
let a be set ; :: thesis: len (k |-> a) = k
reconsider k = k as Element of NAT by ORDINAL1:def 13;
dom (k |-> a) = Seg k by FUNCOP_1:19;
hence len (k |-> a) = k by FINSEQ_1:def 3; :: thesis: verum