let f be non empty FinSequence; :: thesis: ( 1 in dom f & len f in dom f )
A1: len f >= 1 by NAT_1:14;
hence 1 in dom f by FINSEQ_3:25; :: thesis: len f in dom f
thus len f in dom f by A1, FINSEQ_3:25; :: thesis: verum