let i be Nat; :: thesis: for f, g being FinSequence st len f < i & i <= (len f) + (len g) holds
i - (len f) in dom g
let f, g be FinSequence; :: thesis: ( len f < i & i <= (len f) + (len g) implies i - (len f) in dom g )
assume that
A1: len f < i and
A2: i <= (len f) + (len g) ; :: thesis: i - (len f) in dom g
A3: i - (len f) is Element of NAT by A1, INT_1:5;
A4: i - (len f) <= ((len f) + (len g)) - (len f) by A2, XREAL_1:9;
i - (len f) > (len f) - (len f) by A1, XREAL_1:14;
then 1 <= i - (len f) by A3, NAT_1:14;
hence i - (len f) in dom g by A3, A4, FINSEQ_3:25; :: thesis: verum