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