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 :: thesis: for n, m being Element of NAT st n in dom (f | i) & m in dom (f | i) & (f | i) /. n = (f | i) /. m holds
n = m

A2: dom (f | i) c= dom f by Th18;
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:70
.= f /. m by A4, A5, FINSEQ_4:70 ;
hence n = m by A1, A3, A4, A2, PARTFUN2:10; :: thesis: verum

end;

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