theorem Th40: :: FINSEQ_2:42

for p, q being FinSequence
for f being Function of (dom p),(dom p) st rng f = dom p & q = p * f holds
len q = len p