let i be Nat; :: thesis: for D being non empty set
for f being FinSequence of D st i in dom f & f is one-to-one holds
(f /. i) .. f = i
let D be non empty set ; :: thesis: for f being FinSequence of D st i in dom f & f is one-to-one holds
(f /. i) .. f = i
let f be FinSequence of D; :: thesis: ( i in dom f & f is one-to-one implies (f /. i) .. f = i )
assume A1: i in dom f ; :: thesis: ( not f is one-to-one or (f /. i) .. f = i )
assume f is one-to-one ; :: thesis: (f /. i) .. f = i
then (f . i) .. f = i by A1, Th11;
hence (f /. i) .. f = i by A1, PARTFUN1:def 6; :: thesis: verum