theorem Th5: :: INTEGR23:5

for p being FinSequence
for a being object holds
( p = (len p) |-> a iff for k being object st k in dom p holds
p . k = a )