let F be FinSequence; :: thesis: ( F is empty implies F is weakly-one-to-one )
assume Z: F is empty ; :: thesis: F is weakly-one-to-one
let i be Element of NAT ; :: according to JORDAN23:def 2 :: thesis: ( 1 <= i & i < len F implies F . i <> F . (i + 1) )
assume ( 1 <= i & i < len F ) ; :: thesis: F . i <> F . (i + 1)
hence F . i <> F . (i + 1) by Z; :: thesis: verum