set S = 1GateCircStr (<*F₁(),F₂(),F₃()*>,F₆());
let s be State of (1GateCircuit (<*F₁(),F₂(),F₃()*>,F₆())); :: thesis: for a1, a2, a3 being Element of F₄() st a1 = s . F₁() & a2 = s . F₂() & a3 = s . F₃() holds
(Result s) . (Output (1GateCircStr (<*F₁(),F₂(),F₃()*>,F₆()))) = F₅(a1,a2,a3)
A2: dom s = the carrier of (1GateCircStr (<*F₁(),F₂(),F₃()*>,F₆())) by CIRCUIT1:3
.= (rng <*F₁(),F₂(),F₃()*>) \/ {[<*F₁(),F₂(),F₃()*>,F₆()]} by CIRCCOMB:def 6
.= {F₁(),F₂(),F₃()} \/ {[<*F₁(),F₂(),F₃()*>,F₆()]} by FINSEQ_2:128
.= {F₁(),F₂(),F₃(),[<*F₁(),F₂(),F₃()*>,F₆()]} by ENUMSET1:6 ;
then A3: ( F₁() in dom s & F₂() in dom s ) by ENUMSET1:def 2;
A4: F₃() in dom s by A2, ENUMSET1:def 2;
let a1, a2, a3 be Element of F₄(); :: thesis: ( a1 = s . F₁() & a2 = s . F₂() & a3 = s . F₃() implies (Result s) . (Output (1GateCircStr (<*F₁(),F₂(),F₃()*>,F₆()))) = F₅(a1,a2,a3) )
assume ( a1 = s . F₁() & a2 = s . F₂() & a3 = s . F₃() ) ; :: thesis: (Result s) . (Output (1GateCircStr (<*F₁(),F₂(),F₃()*>,F₆()))) = F₅(a1,a2,a3)
then A5: s * <*F₁(),F₂(),F₃()*> = <*a1,a2,a3*> by A3, A4, FINSEQ_2:126;
thus (Result s) . (Output (1GateCircStr (<*F₁(),F₂(),F₃()*>,F₆()))) = (Following s) . (Output (1GateCircStr (<*F₁(),F₂(),F₃()*>,F₆()))) by Th20
.= (Following s) . [<*F₁(),F₂(),F₃()*>,F₆()] by Th15
.= F₆() . (s * <*F₁(),F₂(),F₃()*>) by CIRCCOMB:56
.= F₅(a1,a2,a3) by A1, A5 ; :: thesis: verum