let s be State of (1GateCircuit <*F1(),F2()*>,F5()); :: thesis: 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)
let a1, a2 be Element of F3(); :: thesis: ( a1 = s . F1() & a2 = s . F2() implies (Result s) . (Output (1GateCircStr <*F1(),F2()*>,F5())) = F4(a1,a2) )
assume A2:
( a1 = s . F1() & a2 = s . F2() )
; :: thesis: (Result s) . (Output (1GateCircStr <*F1(),F2()*>,F5())) = F4(a1,a2)
set S = 1GateCircStr <*F1(),F2()*>,F5();
dom s =
the carrier of (1GateCircStr <*F1(),F2()*>,F5())
by CIRCUIT1:4
.=
(rng <*F1(),F2()*>) \/ {[<*F1(),F2()*>,F5()]}
by CIRCCOMB:def 6
.=
{F1(),F2()} \/ {[<*F1(),F2()*>,F5()]}
by FINSEQ_2:147
.=
{F1(),F2(),[<*F1(),F2()*>,F5()]}
by ENUMSET1:43
;
then
( F1() in dom s & F2() in dom s )
by ENUMSET1:def 1;
then A3:
s * <*F1(),F2()*> = <*a1,a2*>
by A2, FINSEQ_2:145;
thus (Result s) . (Output (1GateCircStr <*F1(),F2()*>,F5())) =
(Following s) . (Output (1GateCircStr <*F1(),F2()*>,F5()))
by Th21
.=
(Following s) . [<*F1(),F2()*>,F5()]
by Th16
.=
F5() . (s * <*F1(),F2()*>)
by CIRCCOMB:64
.=
F4(a1,a2)
by A1, A3
; :: thesis: verum