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