consider i being Nat such that
A2:
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);
A3:
InnerVertices H1(k) c= InnerVertices H1(n)
by A1, Th22;
A4:
GFA1AdderOutput (x . k),(y . k),(i -BitGFA1CarryOutput x,y) in InnerVertices H2(i)
by A2, GFACIRC1:82;
A5:
H1(k) = H1(i) +* H2(i)
by A2, Th21;
reconsider o = GFA1AdderOutput (x . k),(y . k),(i -BitGFA1CarryOutput x,y) as Element of H2(i) by A4;
the carrier of H1(k) = the carrier of H2(i) \/ the carrier of H1(i)
by A5, CIRCCOMB:def 2;
then
o in the carrier of H1(k)
by XBOOLE_0:def 3;
then
o in InnerVertices H1(k)
by A4, A5, CIRCCOMB:19;
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 A2, A3; :: thesis: verum