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)
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 A2: ( 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)
set S = 1GateCircStr <*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₈();
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 ( F₁() in dom s & F₂() in dom s & F₃() in dom s & F₄() in dom s & F₅() in dom s ) by ENUMSET1:def 4;
then A3: s * <*F₁(),F₂(),F₃(),F₄(),F₅()*> = <*a1,a2,a3,a4,a5*> by A2, 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, A3 ; :: thesis: verum