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 & ( 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
A8: ( 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 ) ) ) ; :: thesis: s1 = s2
A9: len s1 = n by FINSEQ_1:def 18;
then A10: len s1 = len s2 by FINSEQ_1:def 18;
defpred S₁[ Element of NAT ] means ( 1 <= $1 & $1 <= n - 1 implies s1 . $1 = s2 . $1 );
A11: S₁[ 0 ] ;
A12: for i being Element of NAT st S₁[i] holds
S₁[i + 1]

proof

let kk be Element of NAT ; :: thesis: ( S₁[kk] implies S₁[kk + 1] )
assume A13: ( 1 <= kk & kk <= n - 1 implies s1 . kk = s2 . kk ) ; :: thesis: S₁[kk + 1]
assume A14: ( 1 <= kk + 1 & kk + 1 <= n - 1 ) ; :: thesis: s1 . (kk + 1) = s2 . (kk + 1)
A15: ( 0 = kk or ( 0 < kk & 0 + 1 = 1 ) ) ;

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

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

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

end;

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

A17: kk <= kk + 1 by NAT_1:11;
then A18: ( 1 <= kk & kk <= n - 1 ) by A14, A16, XXREAL_0:2;
then consider i1, i2 being Nat such that
A19: ( i1 = s1 . kk & i2 = s1 . (kk + 1) & i2 = (((i1 |^ (Radix k)) mod f) * (Table2 m,e,f,(n -' kk))) mod f ) by A7;
consider i1, i2 being Nat such that
A20: ( i1 = s2 . kk & i2 = s2 . (kk + 1) & i2 = (((i1 |^ (Radix k)) mod f) * (Table2 m,e,f,(n -' kk))) mod f ) by A8, A18;
thus s1 . (kk + 1) = s2 . (kk + 1) by A13, A14, A16, A17, A19, A20, XXREAL_0:2; :: thesis: verum

end;

end;

end;

A21: for kk being Element of NAT holds S₁[kk] from NAT_1:sch 1(A11, A12);
A22: s1 . n = s2 . n

proof

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

now

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

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

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

end;

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

then A23: ( 1 <= U1 & U1 <= U1 ) by NAT_1:14;
then consider i1, i2 being Nat such that
A24: ( i1 = s1 . U1 & i2 = s1 . (U1 + 1) ) and
A25: i2 = (((i1 |^ (Radix k)) mod f) * (Table2 m,e,f,(n -' U1))) mod f by A7;
consider j1, j2 being Nat such that
A26: ( j1 = s2 . U1 & j2 = s2 . (U1 + 1) ) and
A27: j2 = (((j1 |^ (Radix k)) mod f) * (Table2 m,e,f,(n -' U1))) mod f by A8, A23;
thus s1 . n = s2 . n by A21, A23, A24, A25, A26, A27; :: thesis: verum

end;

end;

end;

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

end;

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 A28: ( 1 <= kk & kk <= len s1 ) ; :: thesis: s1 . kk = s2 . kk
A29: kk in NAT by ORDINAL1:def 13;

now

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

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

n - 1 >= 1 - 1 by A1, XREAL_1:11;
then reconsider U1 = (len s1) - 1 as Element of NAT by A9, INT_1:16;
U1 + 1 = len s1 ;
then kk <= U1 by A30, NAT_1:13;
hence s1 . kk = s2 . kk by A9, A21, A28, A29; :: thesis: verum

end;

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

hence s1 . kk = s2 . kk by A9, A22; :: thesis: verum

end;

end;

end;

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

end;

hence s1 = s2 by A10, FINSEQ_1:18; :: thesis: verum