theorem :: FINSEQ_1:54

for n being Nat holds Seg n,n are_equipotent by Lm1;