let a, n, m be Element of NAT ; :: thesis: ex A, B being sequence of NAT st
( A . 0 = a mod m & B . 0 = 1 & ( for i being Nat holds
( A . (i + 1) = ((A . i) * (A . i)) mod m & B . (i + 1) = BinBranch ((B . i),(((B . i) * (A . i)) mod m),((Nat2BL . n) . (i + 1))) ) ) )
defpred S₁[ Nat, Nat, Nat, Nat, Nat] means ( $4 = ($2 * $2) mod m & $5 = BinBranch ($3,(($3 * $2) mod m),((Nat2BL . n) . ($1 + 1))) );
A1: for i being Nat
for x, y being Element of NAT ex x1, y1 being Element of NAT st S₁[i,x,y,x1,y1]

proof

let i be Nat; :: thesis: for x, y being Element of NAT ex x1, y1 being Element of NAT st S₁[i,x,y,x1,y1]
let x, y be Element of NAT ; :: thesis: ex x1, y1 being Element of NAT st S₁[i,x,y,x1,y1]
set x1 = (x * x) mod m;
set y1 = BinBranch (y,((y * x) mod m),((Nat2BL . n) . (i + 1)));
( (x * x) mod m is Element of NAT & BinBranch (y,((y * x) mod m),((Nat2BL . n) . (i + 1))) is Element of NAT ) by ORDINAL1:def 12;
hence ex x1, y1 being Element of NAT st S₁[i,x,y,x1,y1] ; :: thesis: verum

end;

consider A, B being sequence of NAT such that
A2: ( A . 0 = a mod m & B . 0 = 1 & ( for n being Nat holds S₁[n,A . n,B . n,A . (n + 1),B . (n + 1)] ) ) from RECDEF_2:sch 3(A1);
take A ; :: thesis: ex B being sequence of NAT st
( A . 0 = a mod m & B . 0 = 1 & ( for i being Nat holds
( A . (i + 1) = ((A . i) * (A . i)) mod m & B . (i + 1) = BinBranch ((B . i),(((B . i) * (A . i)) mod m),((Nat2BL . n) . (i + 1))) ) ) )
take B ; :: thesis: ( A . 0 = a mod m & B . 0 = 1 & ( for i being Nat holds
( A . (i + 1) = ((A . i) * (A . i)) mod m & B . (i + 1) = BinBranch ((B . i),(((B . i) * (A . i)) mod m),((Nat2BL . n) . (i + 1))) ) ) )
thus ( A . 0 = a mod m & B . 0 = 1 & ( for i being Nat holds
( A . (i + 1) = ((A . i) * (A . i)) mod m & B . (i + 1) = BinBranch ((B . i),(((B . i) * (A . i)) mod m),((Nat2BL . n) . (i + 1))) ) ) ) by A2; :: thesis: verum