theorem :: NAT_3:10

for f being FinSequence of REAL holds f |^ 1 = f