let p, q be FinSequence of NAT ; :: thesis: for f being Element of REAL *
for i, n being Element of NAT st ( for k being Nat st 1 <= k & k < len p holds
p . ((len p) - k) = f . ((p /. (((len p) - k) + 1)) + n) ) & ( for k being Nat st 1 <= k & k < len q holds
q . ((len q) - k) = f . ((q /. (((len q) - k) + 1)) + n) ) & len p <= len q & p . (len p) = q . (len q) holds
for k being Nat st 1 <= k & k < len p holds
p . ((len p) - k) = q . ((len q) - k)
let f be Element of REAL * ; :: thesis: for i, n being Element of NAT st ( for k being Nat st 1 <= k & k < len p holds
p . ((len p) - k) = f . ((p /. (((len p) - k) + 1)) + n) ) & ( for k being Nat st 1 <= k & k < len q holds
q . ((len q) - k) = f . ((q /. (((len q) - k) + 1)) + n) ) & len p <= len q & p . (len p) = q . (len q) holds
for k being Nat st 1 <= k & k < len p holds
p . ((len p) - k) = q . ((len q) - k)
let i, n be Element of NAT ; :: thesis: ( ( for k being Nat st 1 <= k & k < len p holds
p . ((len p) - k) = f . ((p /. (((len p) - k) + 1)) + n) ) & ( for k being Nat st 1 <= k & k < len q holds
q . ((len q) - k) = f . ((q /. (((len q) - k) + 1)) + n) ) & len p <= len q & p . (len p) = q . (len q) implies for k being Nat st 1 <= k & k < len p holds
p . ((len p) - k) = q . ((len q) - k) )
assume that
A1: for k being Nat st 1 <= k & k < len p holds
p . ((len p) - k) = f . ((p /. (((len p) - k) + 1)) + n) and
A2: for k being Nat st 1 <= k & k < len q holds
q . ((len q) - k) = f . ((q /. (((len q) - k) + 1)) + n) and
A3: len p <= len q and
A4: p . (len p) = q . (len q) ; :: thesis: for k being Nat st 1 <= k & k < len p holds
p . ((len p) - k) = q . ((len q) - k)
defpred S₁[ Nat] means ( $1 < len p implies p . ((len p) - $1) = q . ((len q) - $1) );
A5: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A6: S₁[k] ; :: thesis: S₁[k + 1]

now :: thesis: ( k + 1 < len p implies p . ((len p) - (k + 1)) = q . ((len q) - (k + 1)) )

A7: ( k <= k + 1 & (len q) - k <= len q ) by Lm9, NAT_1:11;
assume A8: k + 1 < len p ; :: thesis: p . ((len p) - (k + 1)) = q . ((len q) - (k + 1))
then A9: 1 <= (len p) - k by XREAL_1:19;
(len p) - k <= (len q) - k by A3, XREAL_1:9;
then A10: 1 <= (len q) - k by A9, XXREAL_0:2;
A11: k + 1 < len q by A3, A8, XXREAL_0:2;
A12: p /. ((len p) - k) = p . ((len p) - k) by A9, Lm9, Th3
.= q /. ((len q) - k) by A6, A8, A7, A10, Th3, XXREAL_0:2 ;
thus p . ((len p) - (k + 1)) = f . ((p /. (((len p) - (k + 1)) + 1)) + n) by A1, A8, NAT_1:11
.= f . ((q /. (((len q) - (k + 1)) + 1)) + n) by A12
.= q . ((len q) - (k + 1)) by A2, A11, NAT_1:11 ; :: thesis: verum

end;

hence S₁[k + 1] ; :: thesis: verum

end;

A13: S₁[ 0 ] by A4;
for k being Nat holds S₁[k] from NAT_1:sch 2(A13, A5);
hence for k being Nat st 1 <= k & k < len p holds
p . ((len p) - k) = q . ((len q) - k) ; :: thesis: verum