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)
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 A2: ( a1 = s . F₁() & a2 = s . F₂() & a3 = s . F₃() ) ; :: thesis: (Result s) . (Output (1GateCircStr <*F₁(),F₂(),F₃()*>,F₆())) = F₅(a1,a2,a3)
set S = 1GateCircStr <*F₁(),F₂(),F₃()*>,F₆();
dom s = the carrier of (1GateCircStr <*F₁(),F₂(),F₃()*>,F₆()) by CIRCUIT1:4
.= (rng <*F₁(),F₂(),F₃()*>) \/ {[<*F₁(),F₂(),F₃()*>,F₆()]} by CIRCCOMB:def 6
.= {F₁(),F₂(),F₃()} \/ {[<*F₁(),F₂(),F₃()*>,F₆()]} by FINSEQ_2:148
.= {F₁(),F₂(),F₃(),[<*F₁(),F₂(),F₃()*>,F₆()]} by ENUMSET1:46 ;
then ( F₁() in dom s & F₂() in dom s & F₃() in dom s ) by ENUMSET1:def 2;
then A3: s * <*F₁(),F₂(),F₃()*> = <*a1,a2,a3*> by A2, FINSEQ_2:146;
thus (Result s) . (Output (1GateCircStr <*F₁(),F₂(),F₃()*>,F₆())) = (Following s) . (Output (1GateCircStr <*F₁(),F₂(),F₃()*>,F₆())) by Th21
.= (Following s) . [<*F₁(),F₂(),F₃()*>,F₆()] by Th16
.= F₆() . (s * <*F₁(),F₂(),F₃()*>) by CIRCCOMB:64
.= F₅(a1,a2,a3) by A1, A3 ; :: thesis: verum