consider A, B being sequence of NAT such that

A1: ( 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 Lm1;

set K = B . (LenBSeq n);

B . (LenBSeq n) is Element of NAT ;

hence ex b_{1} being Element of NAT ex A, B being sequence of NAT st

( b_{1} = B . (LenBSeq n) & 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 A1; :: thesis: verum

A1: ( 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 Lm1;

set K = B . (LenBSeq n);

B . (LenBSeq n) is Element of NAT ;

hence ex b

( b

( 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 A1; :: thesis: verum