let f be FinSequence; :: thesis: for k, i being Nat st 1 <= i & i <= k & k <= len f holds

(mid (f,1,k)) . i = f . i

let k, i be Nat; :: thesis: ( 1 <= i & i <= k & k <= len f implies (mid (f,1,k)) . i = f . i )

assume that

A1: 1 <= i and

A2: i <= k and

A3: k <= len f ; :: thesis: (mid (f,1,k)) . i = f . i

A4: i <= (k - 1) + 1 by A2;

1 <= k by A1, A2, XXREAL_0:2;

then (mid (f,1,k)) . i = f . ((i + 1) -' 1) by A1, A3, A4, Th121;

hence (mid (f,1,k)) . i = f . i by NAT_D:34; :: thesis: verum

(mid (f,1,k)) . i = f . i

let k, i be Nat; :: thesis: ( 1 <= i & i <= k & k <= len f implies (mid (f,1,k)) . i = f . i )

assume that

A1: 1 <= i and

A2: i <= k and

A3: k <= len f ; :: thesis: (mid (f,1,k)) . i = f . i

A4: i <= (k - 1) + 1 by A2;

1 <= k by A1, A2, XXREAL_0:2;

then (mid (f,1,k)) . i = f . ((i + 1) -' 1) by A1, A3, A4, Th121;

hence (mid (f,1,k)) . i = f . i by NAT_D:34; :: thesis: verum