let D be non empty set ; :: thesis: for i being Element of NAT
for f being FinSequence of D st 1 <= i & i <= len f holds
(Rev f) . i = f . (((len f) - i) + 1)
let i be Element of NAT ; :: thesis: for f being FinSequence of D st 1 <= i & i <= len f holds
(Rev f) . i = f . (((len f) - i) + 1)
let f be FinSequence of D; :: thesis: ( 1 <= i & i <= len f implies (Rev f) . i = f . (((len f) - i) + 1) )
assume that
A1: 1 <= i and
A2: i <= len f ; :: thesis: (Rev f) . i = f . (((len f) - i) + 1)
i in dom f by A1, A2, FINSEQ_3:25;
hence (Rev f) . i = f . (((len f) - i) + 1) by FINSEQ_5:58; :: thesis: verum