theorem :: MATRIXJ1:59

for n being Nat
for K being Field
for f being FinSequence of NAT holds 1. (K,(f | n)) = (1. (K,f)) | n