theorem Th58: :: FINSEQ_2:60

for i being natural Number
for a being object holds (i + 1) |-> a = (i |-> a) ^ <*a*>