let F be FinSequence; :: thesis: ( F is empty implies F is weakly-one-to-one )
assume A1: 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 that
A2: 1 <= i and
A3: i < len F ; :: thesis: F . i <> F . (i + 1)
thus F . i <> F . (i + 1) by A1, A2, A3; :: thesis: verum