let i be Nat; :: thesis: for D being non empty set
for f being FinSequence of D st f is one-to-one holds
f | i is one-to-one
let D be non empty set ; :: thesis: for f being FinSequence of D st f is one-to-one holds
f | i is one-to-one
let f be FinSequence of D; :: thesis: ( f is one-to-one implies f | i is one-to-one )
assume A1: f is one-to-one ; :: thesis: f | i is one-to-one

now

A2: dom (f | i) c= dom f by Th20;
let n, m be Element of NAT ; :: thesis: ( n in dom (f | i) & m in dom (f | i) & (f | i) /. n = (f | i) /. m implies n = m )
assume that
A3: n in dom (f | i) and
A4: m in dom (f | i) and
A5: (f | i) /. n = (f | i) /. m ; :: thesis: n = m
f /. n = (f | i) /. n by A3, FINSEQ_4:85
.= f /. m by A4, A5, FINSEQ_4:85 ;
hence n = m by A1, A3, A4, A2, PARTFUN2:17; :: thesis: verum

end;

hence f | i is one-to-one by PARTFUN2:16; :: thesis: verum