theorem Th60: :: HILB10_7:60

for i being Nat
for f being FinSequence st i in dom f holds
(App <*f*>) . <*i*> = <*(f . i)*>