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 Element of NAT st 1 <= i & i < len f holds
f . i <> f . (i + 1)

proof

let i be Element of NAT ; :: thesis: ( 1 <= i & i < len f implies f . i <> f . (i + 1) )
assume ( 1 <= i & i < len f ) ; :: thesis: f . i <> f . (i + 1)
then ( i in dom f & i + 1 in dom f & i <> i + 1 ) by MSUALG_8:1;
hence f . i <> f . (i + 1) by A1, FUNCT_1:def 8; :: thesis: verum

end;

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