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