set S = 1GateCircStr <*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₈();
let s be State of (1GateCircuit <*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₈()); :: thesis: for a1, a2, a3, a4, a5 being Element of F₆() st a1 = s . F₁() & a2 = s . F₂() & a3 = s . F₃() & a4 = s . F₄() & a5 = s . F₅() holds
(Result s) . (Output (1GateCircStr <*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₈())) = F₇(a1,a2,a3,a4,a5)
A2: dom s = the carrier of (1GateCircStr <*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₈()) by CIRCUIT1:4
.= (rng <*F₁(),F₂(),F₃(),F₄(),F₅()*>) \/ {[<*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₈()]} by CIRCCOMB:def 6
.= {F₁(),F₂(),F₃(),F₄(),F₅()} \/ {[<*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₈()]} by Th15
.= {F₁(),F₂(),F₃(),F₄(),F₅(),[<*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₈()]} by ENUMSET1:55 ;
then A3: ( F₁() in dom s & F₂() in dom s ) by ENUMSET1:def 4;
A4: F₅() in dom s by A2, ENUMSET1:def 4;
A5: ( F₃() in dom s & F₄() in dom s ) by A2, ENUMSET1:def 4;
let a1, a2, a3, a4, a5 be Element of F₆(); :: thesis: ( a1 = s . F₁() & a2 = s . F₂() & a3 = s . F₃() & a4 = s . F₄() & a5 = s . F₅() implies (Result s) . (Output (1GateCircStr <*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₈())) = F₇(a1,a2,a3,a4,a5) )
assume ( a1 = s . F₁() & a2 = s . F₂() & a3 = s . F₃() & a4 = s . F₄() & a5 = s . F₅() ) ; :: thesis: (Result s) . (Output (1GateCircStr <*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₈())) = F₇(a1,a2,a3,a4,a5)
then A6: s * <*F₁(),F₂(),F₃(),F₄(),F₅()*> = <*a1,a2,a3,a4,a5*> by A3, A5, A4, Th38;
thus (Result s) . (Output (1GateCircStr <*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₈())) = (Following s) . (Output (1GateCircStr <*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₈())) by Th21
.= (Following s) . [<*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₈()] by Th16
.= F₈() . (s * <*F₁(),F₂(),F₃(),F₄(),F₅()*>) by CIRCCOMB:64
.= F₇(a1,a2,a3,a4,a5) by A1, A6 ; :: thesis: verum