let b be object ; :: thesis: for fin being FinSequence holds
( 1 <= len (fin ^ <*b*>) & len (fin ^ <*b*>) in dom (fin ^ <*b*>) )
let fin be FinSequence; :: thesis: ( 1 <= len (fin ^ <*b*>) & len (fin ^ <*b*>) in dom (fin ^ <*b*>) )
len (fin ^ <*b*>) = (len fin) + 1 by FINSEQ_2:16;
then 1 <= len (fin ^ <*b*>) by NAT_1:11;
hence ( 1 <= len (fin ^ <*b*>) & len (fin ^ <*b*>) in dom (fin ^ <*b*>) ) by FINSEQ_3:25; :: thesis: verum