set S = 1GateCircStr (<*F₁()*>,F₆());
let s be State of (F₅() +* (1GateCircuit (<*F₁()*>,F₆()))); :: thesis: for s9 being State of F₅() st s9 = s | the carrier of F₄() holds
for a1 being Element of F₂() st ( F₁() in InnerVertices F₄() implies a1 = (Result s9) . F₁() ) & ( not F₁() in InnerVertices F₄() implies a1 = s . F₁() ) holds
(Result s) . (Output (1GateCircStr (<*F₁()*>,F₆()))) = F₃(a1)
let s9 be State of F₅(); :: thesis: ( s9 = s | the carrier of F₄() implies for a1 being Element of F₂() st ( F₁() in InnerVertices F₄() implies a1 = (Result s9) . F₁() ) & ( not F₁() in InnerVertices F₄() implies a1 = s . F₁() ) holds
(Result s) . (Output (1GateCircStr (<*F₁()*>,F₆()))) = F₃(a1) )
assume A3: s9 = s | the carrier of F₄() ; :: thesis: for a1 being Element of F₂() st ( F₁() in InnerVertices F₄() implies a1 = (Result s9) . F₁() ) & ( not F₁() in InnerVertices F₄() implies a1 = s . F₁() ) holds
(Result s) . (Output (1GateCircStr (<*F₁()*>,F₆()))) = F₃(a1)
rng <*F₁()*> = {F₁()} by FINSEQ_1:38;
then A4: ( InputVertices (1GateCircStr (<*F₁()*>,F₆())) = rng <*F₁()*> & F₁() in rng <*F₁()*> ) by CIRCCOMB:42, TARSKI:def 1;
then A5: ( F₁() in InnerVertices F₄() or F₁() in (InputVertices (1GateCircStr (<*F₁()*>,F₆()))) \ (InnerVertices F₄()) ) by XBOOLE_0:def 5;
A6: s9 is stabilizing by Def2;
InnerVertices (1GateCircStr (<*F₁()*>,F₆())) = {(Output (1GateCircStr (<*F₁()*>,F₆())))} by Th16;
then A7: InputVertices F₄() misses InnerVertices (1GateCircStr (<*F₁()*>,F₆())) by A2, ZFMISC_1:50;
then A8: (Following (s,(stabilization-time s9))) | the carrier of F₄() = Following (s9,(stabilization-time s9)) by A3, Th27, CIRCCMB2:13
.= Result s9 by A6, Th2 ;
F₄() tolerates 1GateCircStr (<*F₁()*>,F₆()) by CIRCCOMB:47;
then InputVertices (F₄() +* (1GateCircStr (<*F₁()*>,F₆()))) = (InputVertices F₄()) \/ ((InputVertices (1GateCircStr (<*F₁()*>,F₆()))) \ (InnerVertices F₄())) by A7, FACIRC_1:4;
then A9: ( F₁() in InnerVertices F₄() or F₁() in InputVertices (F₄() +* (1GateCircStr (<*F₁()*>,F₆()))) ) by A5, XBOOLE_0:def 3;
let a1 be Element of F₂(); :: thesis: ( ( F₁() in InnerVertices F₄() implies a1 = (Result s9) . F₁() ) & ( not F₁() in InnerVertices F₄() implies a1 = s . F₁() ) implies (Result s) . (Output (1GateCircStr (<*F₁()*>,F₆()))) = F₃(a1) )
assume ( ( F₁() in InnerVertices F₄() implies a1 = (Result s9) . F₁() ) & ( not F₁() in InnerVertices F₄() implies a1 = s . F₁() ) ) ; :: thesis: (Result s) . (Output (1GateCircStr (<*F₁()*>,F₆()))) = F₃(a1)
then A10: a1 = (Following (s,(stabilization-time s9))) . F₁() by A9, A8, Th1, FUNCT_1:49;
A11: s is stabilizing by Def2;
the carrier' of (1GateCircStr (<*F₁()*>,F₆())) = {[<*F₁()*>,F₆()]} by CIRCCOMB:def 6;
then ( [<*F₁()*>,F₆()] in {[<*F₁()*>,F₆()]} & the carrier' of (F₄() +* (1GateCircStr (<*F₁()*>,F₆()))) = the carrier' of F₄() \/ {[<*F₁()*>,F₆()]} ) by CIRCCOMB:def 2, TARSKI:def 1;
then reconsider g = [<*F₁()*>,F₆()] as Gate of (F₄() +* (1GateCircStr (<*F₁()*>,F₆()))) by XBOOLE_0:def 3;
A12: the_result_sort_of g = the ResultSort of (F₄() +* (1GateCircStr (<*F₁()*>,F₆()))) . g by MSUALG_1:def 2
.= g by CIRCCOMB:44 ;
A13: g `2 = F<sub>6</sub>() ;
the carrier of (F<sub>4</sub>() +* (1GateCircStr (<*F<sub>1</sub>()*>,F<sub>6</sub>()))) = the carrier of F<sub>4</sub>() \/ the carrier of (1GateCircStr (<*F<sub>1</sub>()*>,F<sub>6</sub>())) by CIRCCOMB:def 2;
then A14: F<sub>1</sub>() in the carrier of (F<sub>4</sub>() +* (1GateCircStr (<*F<sub>1</sub>()*>,F<sub>6</sub>()))) by A4, XBOOLE_0:def 3;
A15: [<*F<sub>1</sub>()*>,F<sub>6</sub>()] = Output (1GateCircStr (<*F<sub>1</sub>()*>,F<sub>6</sub>())) by Th15;
g = [( the Arity of (F<sub>4</sub>() +* (1GateCircStr (<*F<sub>1</sub>()*>,F<sub>6</sub>()))) . g),(g `2)] by CIRCCOMB:def 8;
then A16: <*F₁()*> = the Arity of (F₄() +* (1GateCircStr (<*F₁()*>,F₆()))) . g by XTUPLE_0:1
.= the_arity_of g by MSUALG_1:def 1 ;
dom (Following (s,(stabilization-time s9))) = the carrier of (F₄() +* (1GateCircStr (<*F₁()*>,F₆()))) by CIRCUIT1:3;
then A17: (Following (s,(stabilization-time s9))) * <*F₁()*> = <*a1*> by A14, A10, FINSEQ_2:34;
stabilization-time s <= 1 + (stabilization-time s9) by A2, A3, Th48;
hence (Result s) . (Output (1GateCircStr (<*F₁()*>,F₆()))) = (Following (s,(1 + (stabilization-time s9)))) . (Output (1GateCircStr (<*F₁()*>,F₆()))) by A11, Th5
.= (Following (Following (s,(stabilization-time s9)))) . g by A15, FACIRC_1:12
.= F₆() . ((Following (s,(stabilization-time s9))) * <*F₁()*>) by A12, A16, A13, FACIRC_1:34
.= F₃(a1) by A1, A17 ;
:: thesis: verum