let s1, s2 be Tuple of n, NAT ; :: thesis: ( s1 . 1 = Table2 (m,e,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds

ex i1, i2 being Nat st

( i1 = s1 . i & i2 = s1 . (i + 1) & i2 = (((i1 |^ (Radix k)) mod f) * (Table2 (m,e,f,(n -' i)))) mod f ) ) & s2 . 1 = Table2 (m,e,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds

ex i1, i2 being Nat st

( i1 = s2 . i & i2 = s2 . (i + 1) & i2 = (((i1 |^ (Radix k)) mod f) * (Table2 (m,e,f,(n -' i)))) mod f ) ) implies s1 = s2 )

assume that

A7: s1 . 1 = Table2 (m,e,f,n) and

A8: for i being Nat st 1 <= i & i <= n - 1 holds

ex I1, I2 being Nat st

( I1 = s1 . i & I2 = s1 . (i + 1) & I2 = (((I1 |^ (Radix k)) mod f) * (Table2 (m,e,f,(n -' i)))) mod f ) and

A9: s2 . 1 = Table2 (m,e,f,n) and

A10: for i being Nat st 1 <= i & i <= n - 1 holds

ex I1, I2 being Nat st

( I1 = s2 . i & I2 = s2 . (i + 1) & I2 = (((I1 |^ (Radix k)) mod f) * (Table2 (m,e,f,(n -' i)))) mod f ) ; :: thesis: s1 = s2

defpred S_{1}[ Nat] means ( 1 <= $1 & $1 <= n - 1 implies s1 . $1 = s2 . $1 );

A11: for i being Nat st S_{1}[i] holds

S_{1}[i + 1]

A18: S_{1}[ 0 ]
;

A19: for kk being Nat holds S_{1}[kk]
from NAT_1:sch 2(A18, A11);

A20: s1 . n = s2 . n

s1 . kk = s2 . kk

hence s1 = s2 by A22, FINSEQ_1:14; :: thesis: verum

ex i1, i2 being Nat st

( i1 = s1 . i & i2 = s1 . (i + 1) & i2 = (((i1 |^ (Radix k)) mod f) * (Table2 (m,e,f,(n -' i)))) mod f ) ) & s2 . 1 = Table2 (m,e,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds

ex i1, i2 being Nat st

( i1 = s2 . i & i2 = s2 . (i + 1) & i2 = (((i1 |^ (Radix k)) mod f) * (Table2 (m,e,f,(n -' i)))) mod f ) ) implies s1 = s2 )

assume that

A7: s1 . 1 = Table2 (m,e,f,n) and

A8: for i being Nat st 1 <= i & i <= n - 1 holds

ex I1, I2 being Nat st

( I1 = s1 . i & I2 = s1 . (i + 1) & I2 = (((I1 |^ (Radix k)) mod f) * (Table2 (m,e,f,(n -' i)))) mod f ) and

A9: s2 . 1 = Table2 (m,e,f,n) and

A10: for i being Nat st 1 <= i & i <= n - 1 holds

ex I1, I2 being Nat st

( I1 = s2 . i & I2 = s2 . (i + 1) & I2 = (((I1 |^ (Radix k)) mod f) * (Table2 (m,e,f,(n -' i)))) mod f ) ; :: thesis: s1 = s2

defpred S

A11: for i being Nat st S

S

proof

A17:
len s1 = n
by CARD_1:def 7;
let kk be Nat; :: thesis: ( S_{1}[kk] implies S_{1}[kk + 1] )

assume A12: ( 1 <= kk & kk <= n - 1 implies s1 . kk = s2 . kk ) ; :: thesis: S_{1}[kk + 1]

A13: ( 0 = kk or ( 0 < kk & 0 + 1 = 1 ) ) ;

assume that

1 <= kk + 1 and

A14: kk + 1 <= n - 1 ; :: thesis: s1 . (kk + 1) = s2 . (kk + 1)

end;assume A12: ( 1 <= kk & kk <= n - 1 implies s1 . kk = s2 . kk ) ; :: thesis: S

A13: ( 0 = kk or ( 0 < kk & 0 + 1 = 1 ) ) ;

assume that

1 <= kk + 1 and

A14: kk + 1 <= n - 1 ; :: thesis: s1 . (kk + 1) = s2 . (kk + 1)

per cases
( 0 = kk or 1 <= kk )
by A13, NAT_1:13;

end;

suppose A15:
1 <= kk
; :: thesis: s1 . (kk + 1) = s2 . (kk + 1)

A16:
kk <= kk + 1
by NAT_1:11;

then kk <= n - 1 by A14, XXREAL_0:2;

then ( ex i1, i2 being Nat st

( i1 = s1 . kk & i2 = s1 . (kk + 1) & i2 = (((i1 |^ (Radix k)) mod f) * (Table2 (m,e,f,(n -' kk)))) mod f ) & ex i1, i2 being Nat st

( i1 = s2 . kk & i2 = s2 . (kk + 1) & i2 = (((i1 |^ (Radix k)) mod f) * (Table2 (m,e,f,(n -' kk)))) mod f ) ) by A8, A10, A15;

hence s1 . (kk + 1) = s2 . (kk + 1) by A12, A14, A15, A16, XXREAL_0:2; :: thesis: verum

end;then kk <= n - 1 by A14, XXREAL_0:2;

then ( ex i1, i2 being Nat st

( i1 = s1 . kk & i2 = s1 . (kk + 1) & i2 = (((i1 |^ (Radix k)) mod f) * (Table2 (m,e,f,(n -' kk)))) mod f ) & ex i1, i2 being Nat st

( i1 = s2 . kk & i2 = s2 . (kk + 1) & i2 = (((i1 |^ (Radix k)) mod f) * (Table2 (m,e,f,(n -' kk)))) mod f ) ) by A8, A10, A15;

hence s1 . (kk + 1) = s2 . (kk + 1) by A12, A14, A15, A16, XXREAL_0:2; :: thesis: verum

A18: S

A19: for kk being Nat holds S

A20: s1 . n = s2 . n

proof

A22:
for kk being Nat st 1 <= kk & kk <= len s1 holds
n - 1 >= 1 - 1
by A1, XREAL_1:9;

then reconsider U1 = n - 1 as Element of NAT by INT_1:3;

end;then reconsider U1 = n - 1 as Element of NAT by INT_1:3;

now :: thesis: s1 . n = s2 . nend;

hence
s1 . n = s2 . n
; :: thesis: verumper cases
( U1 = 0 or 0 < U1 )
;

end;

suppose
0 < U1
; :: thesis: s1 . n = s2 . n

then A21:
1 <= U1
by NAT_1:14;

then ( ex i1, i2 being Nat st

( i1 = s1 . U1 & i2 = s1 . (U1 + 1) & i2 = (((i1 |^ (Radix k)) mod f) * (Table2 (m,e,f,(n -' U1)))) mod f ) & ex j1, j2 being Nat st

( j1 = s2 . U1 & j2 = s2 . (U1 + 1) & j2 = (((j1 |^ (Radix k)) mod f) * (Table2 (m,e,f,(n -' U1)))) mod f ) ) by A8, A10;

hence s1 . n = s2 . n by A19, A21; :: thesis: verum

end;then ( ex i1, i2 being Nat st

( i1 = s1 . U1 & i2 = s1 . (U1 + 1) & i2 = (((i1 |^ (Radix k)) mod f) * (Table2 (m,e,f,(n -' U1)))) mod f ) & ex j1, j2 being Nat st

( j1 = s2 . U1 & j2 = s2 . (U1 + 1) & j2 = (((j1 |^ (Radix k)) mod f) * (Table2 (m,e,f,(n -' U1)))) mod f ) ) by A8, A10;

hence s1 . n = s2 . n by A19, A21; :: thesis: verum

s1 . kk = s2 . kk

proof

len s1 = len s2
by A17, CARD_1:def 7;
let kk be Nat; :: thesis: ( 1 <= kk & kk <= len s1 implies s1 . kk = s2 . kk )

assume that

A23: 1 <= kk and

A24: kk <= len s1 ; :: thesis: s1 . kk = s2 . kk

end;assume that

A23: 1 <= kk and

A24: kk <= len s1 ; :: thesis: s1 . kk = s2 . kk

now :: thesis: s1 . kk = s2 . kkend;

hence
s1 . kk = s2 . kk
; :: thesis: verumper cases
( kk < len s1 or kk = len s1 )
by A24, XXREAL_0:1;

end;

hence s1 = s2 by A22, FINSEQ_1:14; :: thesis: verum