let f be FinSequence; :: thesis: ( f is one-to-one implies f is weakly-one-to-one )
assume A1: f is one-to-one ; :: thesis: f is weakly-one-to-one
for i being Nat st 1 <= i & i < len f holds
f . i <> f . (i + 1)

proof

let i be Nat; :: thesis: ( 1 <= i & i < len f implies f . i <> f . (i + 1) )
assume that
A2: 1 <= i and
A3: i < len f ; :: thesis: f . i <> f . (i + 1)
A4: i + 1 in dom f by A2, A3, MSUALG_8:1;
A5: i <> i + 1 ;
i in dom f by A2, A3, MSUALG_8:1;
hence f . i <> f . (i + 1) by A1, A4, A5; :: thesis: verum

end;

hence f is weakly-one-to-one ; :: thesis: verum