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: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 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: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, A5 ; :: thesis: verum