let p be 1-sorted-yielding FinSequence; :: thesis: len (Carrier p) = len p
dom (Carrier p) = dom p by Def13;
hence len (Carrier p) = len p by FINSEQ_3:29; :: thesis: verum