theorem Lem10: :: SRINGS_3:1

for f1, f2 being FinSequence
for k being Nat st k in Seg ((len f1) * (len f2)) holds
( ((k -' 1) mod (len f2)) + 1 in dom f2 & ((k -' 1) div (len f2)) + 1 in dom f1 )