set S = 1GateCircStr (<*F₁()*>,F₄());
let s be State of (1GateCircuit (<*F₁()*>,F₄())); :: thesis: for a1 being Element of F₂() st a1 = s . F₁() holds
(Result s) . (Output (1GateCircStr (<*F₁()*>,F₄()))) = F₃(a1)
dom s = the carrier of (1GateCircStr (<*F₁()*>,F₄())) by CIRCUIT1:3
.= (rng <*F₁()*>) \/ {[<*F₁()*>,F₄()]} by CIRCCOMB:def 6
.= {F₁()} \/ {[<*F₁()*>,F₄()]} by FINSEQ_1:38
.= {F₁(),[<*F₁()*>,F₄()]} by ENUMSET1:1 ;
then A2: F₁() in dom s by TARSKI:def 2;
let a1 be Element of F₂(); :: thesis: ( a1 = s . F₁() implies (Result s) . (Output (1GateCircStr (<*F₁()*>,F₄()))) = F₃(a1) )
assume a1 = s . F₁() ; :: thesis: (Result s) . (Output (1GateCircStr (<*F₁()*>,F₄()))) = F₃(a1)
then A3: s * <*F₁()*> = <*a1*> by A2, FINSEQ_2:34;
thus (Result s) . (Output (1GateCircStr (<*F₁()*>,F₄()))) = (Following s) . (Output (1GateCircStr (<*F₁()*>,F₄()))) by Th20
.= (Following s) . [<*F₁()*>,F₄()] by Th15
.= F₄() . (s * <*F₁()*>) by CIRCCOMB:56
.= F₃(a1) by A1, A3 ; :: thesis: verum