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 -BitGFA0Str x,y;
deffunc H2( Nat) -> ManySortedSign = BitGFA0Str (x . ($1 + 1)),(y . ($1 + 1)),($1 -BitGFA0CarryOutput x,y);
set o = GFA0AdderOutput (x . k),(y . k),(i -BitGFA0CarryOutput x,y);
A4:
InnerVertices H1(k) c= InnerVertices H1(n)
by A2, Th8;
A5:
GFA0AdderOutput (x . k),(y . k),(i -BitGFA0CarryOutput x,y) in InnerVertices H2(i)
by A3, GFACIRC1:45;
A6:
H1(k) = H1(i) +* H2(i)
by A3, Th7;
reconsider o = GFA0AdderOutput (x . k),(y . k),(i -BitGFA0CarryOutput 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:19;
hence
ex b1 being Element of InnerVertices (n -BitGFA0Str x,y) ex i being Nat st
( k = i + 1 & b1 = GFA0AdderOutput (x . k),(y . k),(i -BitGFA0CarryOutput x,y) )
by A3, A4; verum