deffunc H1( set ) -> non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign = F1(\$1);
A7: for n being Nat
for S being non empty ManySortedSign
for x being set st S = H1(n) & x = F2() . n holds
( H1(n + 1) = S +* F3(x,n) & F2() . (n + 1) = F4(x,n) & x in InputVertices F3(x,n) & F4(x,n) in InnerVertices F3(x,n) ) by A6;
let n be Nat; :: thesis: ( InputVertices F1((n + 1)) = (InputVertices F1(n)) \/ ((InputVertices F3((F2() . n),n)) \ {(F2() . n)}) & InnerVertices F1(n) is Relation & InputVertices F1(n) is without_pairs )
A8: for n being Nat
for x being set st x = F2() . n holds
(InputVertices F3(x,n)) \ {x} is without_pairs by A5;
A9: ( H1( 0 ) = H1( 0 ) & F2() . 0 in InnerVertices H1( 0 ) ) by A3;
A10: for n being Nat
for x being set holds InnerVertices F3(x,n) is Relation by A4;
for n being Nat ex S1, S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st
( S1 = H1(n) & S2 = H1(n + 1) & InputVertices S2 = () \/ ((InputVertices F3((F2() . n),n)) \ {(F2() . n)}) & InnerVertices S1 is Relation & InputVertices S1 is without_pairs ) from CIRCCMB2:sch 10(A1, A2, A9, A10, A8, A7);
then ex S1, S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st
( S1 = F1(n) & S2 = F1((n + 1)) & InputVertices S2 = () \/ ((InputVertices F3((F2() . n),n)) \ {(F2() . n)}) & InnerVertices S1 is Relation & InputVertices S1 is without_pairs ) ;
hence ( InputVertices F1((n + 1)) = (InputVertices F1(n)) \/ ((InputVertices F3((F2() . n),n)) \ {(F2() . n)}) & InnerVertices F1(n) is Relation & InputVertices F1(n) is without_pairs ) ; :: thesis: verum