consider i being Nat such that
A3:
k = 1 + i
by A1, NAT_1:10;
reconsider i = i as Nat ;
deffunc H1( Nat) -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign = $1 -BitGFA1Str (x,y);
deffunc H2( Nat) -> ManySortedSign = BitGFA1Str ((x . ($1 + 1)),(y . ($1 + 1)),($1 -BitGFA1CarryOutput (x,y)));
set o = GFA1AdderOutput ((x . k),(y . k),(i -BitGFA1CarryOutput (x,y)));
A4:
InnerVertices H1(k) c= InnerVertices H1(n)
by A2, Th22;
A5:
GFA1AdderOutput ((x . k),(y . k),(i -BitGFA1CarryOutput (x,y))) in InnerVertices H2(i)
by A3, GFACIRC1:69;
A6:
H1(k) = H1(i) +* H2(i)
by A3, Th21;
reconsider o = GFA1AdderOutput ((x . k),(y . k),(i -BitGFA1CarryOutput (x,y))) as Element of H2(i) by A5;
the carrier of H1(k) = the carrier of H2(i) \/ the carrier of H1(i)
by A6, CIRCCOMB:def 2;
then
o in the carrier of H1(k)
by XBOOLE_0:def 3;
then
o in InnerVertices H1(k)
by A5, A6, CIRCCOMB:15;
hence
ex b1 being Element of InnerVertices (n -BitGFA1Str (x,y)) ex i being Nat st
( k = i + 1 & b1 = GFA1AdderOutput ((x . k),(y . k),(i -BitGFA1CarryOutput (x,y))) )
by A3, A4; verum