let a, n, m be Element of NAT ; :: thesis: for A1, B1, A2, B2 being sequence of NAT st A1 . 0 = a & B1 . 0 = 1 & ( for i being Nat holds
( A1 . (i + 1) = ((A1 . i) * (A1 . i)) mod m & B1 . (i + 1) = BinBranch ((B1 . i),(((B1 . i) * (A1 . i)) mod m),((Nat2BL . n) . (i + 1))) ) ) & A2 . 0 = a & B2 . 0 = 1 & ( for i being Nat holds
( A2 . (i + 1) = ((A2 . i) * (A2 . i)) mod m & B2 . (i + 1) = BinBranch ((B2 . i),(((B2 . i) * (A2 . i)) mod m),((Nat2BL . n) . (i + 1))) ) ) holds
( A1 = A2 & B1 = B2 )
let A1, B1, A2, B2 be sequence of NAT; :: thesis: ( A1 . 0 = a & B1 . 0 = 1 & ( for i being Nat holds
( A1 . (i + 1) = ((A1 . i) * (A1 . i)) mod m & B1 . (i + 1) = BinBranch ((B1 . i),(((B1 . i) * (A1 . i)) mod m),((Nat2BL . n) . (i + 1))) ) ) & A2 . 0 = a & B2 . 0 = 1 & ( for i being Nat holds
( A2 . (i + 1) = ((A2 . i) * (A2 . i)) mod m & B2 . (i + 1) = BinBranch ((B2 . i),(((B2 . i) * (A2 . i)) mod m),((Nat2BL . n) . (i + 1))) ) ) implies ( A1 = A2 & B1 = B2 ) )
assume A1: ( A1 . 0 = a & B1 . 0 = 1 & ( for i being Nat holds
( A1 . (i + 1) = ((A1 . i) * (A1 . i)) mod m & B1 . (i + 1) = BinBranch ((B1 . i),(((B1 . i) * (A1 . i)) mod m),((Nat2BL . n) . (i + 1))) ) ) ) ; :: thesis: ( not A2 . 0 = a or not B2 . 0 = 1 or ex i being Nat st
( A2 . (i + 1) = ((A2 . i) * (A2 . i)) mod m implies not B2 . (i + 1) = BinBranch ((B2 . i),(((B2 . i) * (A2 . i)) mod m),((Nat2BL . n) . (i + 1))) ) or ( A1 = A2 & B1 = B2 ) )
assume A2: ( A2 . 0 = a & B2 . 0 = 1 & ( for i being Nat holds
( A2 . (i + 1) = ((A2 . i) * (A2 . i)) mod m & B2 . (i + 1) = BinBranch ((B2 . i),(((B2 . i) * (A2 . i)) mod m),((Nat2BL . n) . (i + 1))) ) ) ) ; :: thesis: ( A1 = A2 & B1 = B2 )
defpred S₁[ Nat] means ( A1 . $1 = A2 . $1 & B1 . $1 = B2 . $1 );
A3: S₁[ 0 ] by A1, A2;
A4: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A5: S₁[i] ; :: thesis: S₁[i + 1]
A6: A1 . (i + 1) = ((A1 . i) * (A1 . i)) mod m by A1
.= A2 . (i + 1) by A2, A5 ;
B1 . (i + 1) = BinBranch ((B1 . i),(((B1 . i) * (A1 . i)) mod m),((Nat2BL . n) . (i + 1))) by A1
.= B2 . (i + 1) by A2, A5 ;
hence S₁[i + 1] by A6; :: thesis: verum

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A3, A4);
hence ( A1 = A2 & B1 = B2 ) ; :: thesis: verum