theorem :: JORDAN8:2

for m being Nat
for D being non empty set
for f being FinSequence of D
for G being Matrix of D st f is_sequence_on G holds
f /^ m is_sequence_on G