let m be Element of NAT ; :: thesis: ALGO_BPOW (0,0,m) = 1
consider A, B being sequence of NAT such that
ASC: ( ALGO_BPOW (0,0,m) = B . (LenBSeq 0) & A . 0 = 0 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 . 0) . (i + 1))) ) ) ) by Def1;
ALGO_BPOW (0,0,m) = B . 1 by ASC, BINARI_6:def 1
.= BinBranch ((B . 0),(((B . 0) * (A . 0)) mod m),((Nat2BL . 0) . (0 + 1))) by ASC
.= 1 by ASC, defBB, zerobs ;
hence ALGO_BPOW (0,0,m) = 1 ; :: thesis: verum