theorem Th1: :: NUMERAL1:1

for k, l, m being Nat holds (k (#) (l GeoSeq)) | m is XFinSequence of NAT