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)
let a1 be Element of F₂(); :: thesis: ( a1 = s . F₁() implies (Result s) . (Output (1GateCircStr <*F₁()*>,F₄())) = F₃(a1) )
assume A2: a1 = s . F₁() ; :: thesis: (Result s) . (Output (1GateCircStr <*F₁()*>,F₄())) = F₃(a1)
set S = 1GateCircStr <*F₁()*>,F₄();
dom s = the carrier of (1GateCircStr <*F₁()*>,F₄()) by CIRCUIT1:4
.= (rng <*F₁()*>) \/ {[<*F₁()*>,F₄()]} by CIRCCOMB:def 6
.= {F₁()} \/ {[<*F₁()*>,F₄()]} by FINSEQ_1:55
.= {F₁(),[<*F₁()*>,F₄()]} by ENUMSET1:41 ;
then F₁() in dom s by TARSKI:def 2;
then A3: s * <*F₁()*> = <*a1*> by A2, Th36;
thus (Result s) . (Output (1GateCircStr <*F₁()*>,F₄())) = (Following s) . (Output (1GateCircStr <*F₁()*>,F₄())) by Th21
.= (Following s) . [<*F₁()*>,F₄()] by Th16
.= F₄() . (s * <*F₁()*>) by CIRCCOMB:64
.= F₃(a1) by A1, A3 ; :: thesis: verum