set S = 1GateCircStr (<*F₁(),F₂(),F₃(),F₄()*>,F₇());
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)
A2: dom s = the carrier of (1GateCircStr (<*F₁(),F₂(),F₃(),F₄()*>,F₇())) by CIRCUIT1:3
.= (rng <*F₁(),F₂(),F₃(),F₄()*>) \/ {[<*F₁(),F₂(),F₃(),F₄()*>,F₇()]} by CIRCCOMB:def 6
.= {F₁(),F₂(),F₃(),F₄()} \/ {[<*F₁(),F₂(),F₃(),F₄()*>,F₇()]} by Th13
.= {[<*F₁(),F₂(),F₃(),F₄()*>,F₇()],F₁(),F₂(),F₃(),F₄()} by ENUMSET1:7 ;
then A3: ( F₁() in dom s & F₂() in dom s ) by ENUMSET1:def 3;
A4: ( F₃() in dom s & F₄() in dom s ) by A2, ENUMSET1:def 3;
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 ( 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)
then A5: s * <*F₁(),F₂(),F₃(),F₄()*> = <*a1,a2,a3,a4*> by A3, A4, Th33;
thus (Result s) . (Output (1GateCircStr (<*F₁(),F₂(),F₃(),F₄()*>,F₇()))) = (Following s) . (Output (1GateCircStr (<*F₁(),F₂(),F₃(),F₄()*>,F₇()))) by Th20
.= (Following s) . [<*F₁(),F₂(),F₃(),F₄()*>,F₇()] by Th15
.= F₇() . (s * <*F₁(),F₂(),F₃(),F₄()*>) by CIRCCOMB:56
.= F₆(a1,a2,a3,a4) by A1, A5 ; :: thesis: verum