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