theorem :: FILEREC1:16

for a, b, c being set
for D being non empty set
for f being FinSequence of D st f = <*a,b,c*> holds
f /^ 2 = <*c*>