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₁[ Nat] means ( 1 <= $1 & $1 <= n - 1 implies s1 . $1 = s2 . $1 );
A11: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let kk be Nat; :: thesis: ( S₁[kk] implies S₁[kk + 1] )
assume A12: ( 1 <= kk & kk <= n - 1 implies s1 . kk = s2 . kk ) ; :: thesis: S₁[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)

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

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

hence s1 . (kk + 1) = s2 . (kk + 1) by A7, A9; :: thesis: verum

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;

end;

end;

A17: len s1 = n by CARD_1:def 7;
A18: S₁[ 0 ] ;
A19: for kk being Nat holds S₁[kk] from NAT_1:sch 2(A18, A11);
A20: s1 . n = s2 . n

proof

n - 1 >= 1 - 1 by A1, XREAL_1:9;
then reconsider U1 = n - 1 as Element of NAT by INT_1:3;

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

per cases ( U1 = 0 or 0 < U1 ) ;

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

hence s1 . n = s2 . n by A7, A9; :: thesis: verum

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;

end;

end;

hence s1 . n = s2 . n ; :: thesis: verum

end;

A22: for kk being Nat st 1 <= kk & kk <= len s1 holds
s1 . kk = s2 . kk

proof

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

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

per cases ( kk < len s1 or kk = len s1 ) by A24, XXREAL_0:1;

suppose A25: kk < len s1 ; :: thesis: s1 . kk = s2 . kk

n - 1 >= 1 - 1 by A1, XREAL_1:9;
then reconsider U1 = (len s1) - 1 as Element of NAT by A17, INT_1:3;
U1 + 1 = len s1 ;
then kk <= U1 by A25, NAT_1:13;
hence s1 . kk = s2 . kk by A17, A19, A23; :: thesis: verum

end;

suppose kk = len s1 ; :: thesis: s1 . kk = s2 . kk

hence s1 . kk = s2 . kk by A17, A20; :: thesis: verum

end;

end;

end;

hence s1 . kk = s2 . kk ; :: thesis: verum

end;

len s1 = len s2 by A17, CARD_1:def 7;
hence s1 = s2 by A22, FINSEQ_1:14; :: thesis: verum