deffunc H1( Element of 2 -tuples_on F3()) -> Element of F3() = F4(($1 . 1),($1 . 2));
consider g being Function of (2 -tuples_on F3()),F3() such that
A1: for a being Element of 2 -tuples_on F3() holds g . a = H1(a) from FUNCT_2:sch 4();
 reconsider S = 1GateCircStr (<*F1(),F2()*>,g) as one-gate ManySortedSign ;
take S ; :: thesis: ex A being one-gate Circuit of S st
( InputVertices S = {F1(),F2()} & ( for s being State of A holds (Result s) . (Output S) = F4((s . F1()),(s . F2())) ) )
reconsider A = 1GateCircuit (<*F1(),F2()*>,g) as one-gate Circuit of S ;
take A ; :: thesis: ( InputVertices S = {F1(),F2()} & ( for s being State of A holds (Result s) . (Output S) = F4((s . F1()),(s . F2())) ) )
rng <*F1(),F2()*> = {F1(),F2()} by FINSEQ_2:127;
hence InputVertices S = {F1(),F2()} by CIRCCOMB:42; :: thesis: for s being State of A holds (Result s) . (Output S) = F4((s . F1()),(s . F2()))
let s be State of A; :: thesis: (Result s) . (Output S) = F4((s . F1()),(s . F2()))
reconsider sx = s * <*F1(),F2()*> as Element of 2 -tuples_on F3() by Th12;
A2: dom <*F1(),F2()*> = Seg 2 by FINSEQ_1:89;
then A3: 1 in dom <*F1(),F2()*> by FINSEQ_1:1;
A4: 2 in dom <*F1(),F2()*> by A2, FINSEQ_1:1;
Result s = Following s by Th20;
hence (Result s) . (Output S) = (Following s) . [<*F1(),F2()*>,g] by Th15
.= g . (s * <*F1(),F2()*>) by CIRCCOMB:56
.= F4((sx . 1),(sx . 2)) by A1
.= F4((s . (<*F1(),F2()*> . 1)),(sx . 2)) by A3, FUNCT_1:13
.= F4((s . (<*F1(),F2()*> . 1)),(s . (<*F1(),F2()*> . 2))) by A4, FUNCT_1:13
.= F4((s . F1()),(s . (<*F1(),F2()*> . 2)))
.= F4((s . F1()),(s . F2())) ;
:: thesis: verum