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