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

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
A2: n in dom (f /^ i) and
A3: m in dom (f /^ i) and
A4: (f /^ i) . n = (f /^ i) . m ; :: thesis: n = m
A5: ( i + n in dom f & i + m in dom f ) by A2, A3, Th26;
f . (i + n) = (f /^ i) . n by A2, Th27
.= f . (i + m) by A3, A4, Th27 ;
then i + n = i + m by A1, A5;
hence n = m ; :: thesis: verum

end;

hence f /^ i is one-to-one ; :: thesis: verum