let n be Nat; :: thesis: for a being object holds len (n |-> a) = n
let a be object ; :: thesis: len (n |-> a) = n
set x = n |-> a;
dom (n |-> a) = Seg (len (n |-> a)) by FINSEQ_1:def 3;
hence len (n |-> a) = n by FINSEQ_1:6, FUNCOP_1:13; :: thesis: verum