let p, q be FinSequence of NAT ; 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 * ; 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 ; ( ( 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)
; for k being Nat st 1 <= k & k < len p holds
p . ((len p) - k) = q . ((len q) - k)
defpred S1[ Nat] means ( $1 < len p implies p . ((len p) - $1) = q . ((len q) - $1) );
A5:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A6:
S1[
k]
;
S1[k + 1]
now ( 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
;
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
;
verum end;
hence
S1[
k + 1]
;
verum
end;
A13:
S1[ 0 ]
by A4;
for k being Nat holds S1[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)
; verum