deffunc H₁( Element of 5 -tuples_on F₆()) -> Element of F₆() = F₇(($1 . 1),($1 . 2),($1 . 3),($1 . 4),($1 . 5));
consider g being Function of (5 -tuples_on F₆()),F₆() such that
A1: for a being Element of 5 -tuples_on F₆() holds g . a = H₁(a) from FUNCT_2:sch 4();
reconsider S = 1GateCircStr <*F₁(),F₂(),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₃(),F₄(),F₅()} & ( for s being State of A holds (Result s) . (Output S) = F₇((s . F₁()),(s . F₂()),(s . F₃()),(s . F₄()),(s . F₅())) ) )
reconsider A = 1GateCircuit <*F₁(),F₂(),F₃(),F₄(),F₅()*>,g as one-gate Circuit of S ;
take A ; :: thesis: ( InputVertices S = {F₁(),F₂(),F₃(),F₄(),F₅()} & ( for s being State of A holds (Result s) . (Output S) = F₇((s . F₁()),(s . F₂()),(s . F₃()),(s . F₄()),(s . F₅())) ) )
rng <*F₁(),F₂(),F₃(),F₄(),F₅()*> = {F₁(),F₂(),F₃(),F₄(),F₅()} by Th15;
hence InputVertices S = {F₁(),F₂(),F₃(),F₄(),F₅()} by CIRCCOMB:49; :: thesis: for s being State of A holds (Result s) . (Output S) = F₇((s . F₁()),(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₃()),(s . F₄()),(s . F₅()))
reconsider sx = s * <*F₁(),F₂(),F₃(),F₄(),F₅()*> as Element of 5 -tuples_on F₆() by Th13;
dom <*F₁(),F₂(),F₃(),F₄(),F₅()*> = Seg 5 by FINSEQ_4:94;
then A2: ( 1 in dom <*F₁(),F₂(),F₃(),F₄(),F₅()*> & 2 in dom <*F₁(),F₂(),F₃(),F₄(),F₅()*> & 3 in dom <*F₁(),F₂(),F₃(),F₄(),F₅()*> & 4 in dom <*F₁(),F₂(),F₃(),F₄(),F₅()*> & 5 in dom <*F₁(),F₂(),F₃(),F₄(),F₅()*> ) by FINSEQ_1:3;
Result s = Following s by Th21;
hence (Result s) . (Output S) = (Following s) . [<*F₁(),F₂(),F₃(),F₄(),F₅()*>,g] by Th16
.= g . (s * <*F₁(),F₂(),F₃(),F₄(),F₅()*>) by CIRCCOMB:64
.= F₇((sx . 1),(sx . 2),(sx . 3),(sx . 4),(sx . 5)) by A1
.= F₇((s . (<*F₁(),F₂(),F₃(),F₄(),F₅()*> . 1)),(sx . 2),(sx . 3),(sx . 4),(sx . 5)) by A2, FUNCT_1:23
.= F₇((s . F₁()),(sx . 2),(sx . 3),(sx . 4),(sx . 5)) by FINSEQ_4:93
.= F₇((s . F₁()),(s . (<*F₁(),F₂(),F₃(),F₄(),F₅()*> . 2)),(sx . 3),(sx . 4),(sx . 5)) by A2, FUNCT_1:23
.= F₇((s . F₁()),(s . F₂()),(sx . 3),(sx . 4),(sx . 5)) by FINSEQ_4:93
.= F₇((s . F₁()),(s . F₂()),(s . (<*F₁(),F₂(),F₃(),F₄(),F₅()*> . 3)),(sx . 4),(sx . 5)) by A2, FUNCT_1:23
.= F₇((s . F₁()),(s . F₂()),(s . F₃()),(sx . 4),(sx . 5)) by FINSEQ_4:93
.= F₇((s . F₁()),(s . F₂()),(s . F₃()),(s . (<*F₁(),F₂(),F₃(),F₄(),F₅()*> . 4)),(sx . 5)) by A2, FUNCT_1:23
.= F₇((s . F₁()),(s . F₂()),(s . F₃()),(s . F₄()),(sx . 5)) by FINSEQ_4:93
.= F₇((s . F₁()),(s . F₂()),(s . F₃()),(s . F₄()),(s . (<*F₁(),F₂(),F₃(),F₄(),F₅()*> . 5))) by A2, FUNCT_1:23
.= F₇((s . F₁()),(s . F₂()),(s . F₃()),(s . F₄()),(s . F₅())) by FINSEQ_4:93 ;
:: thesis: verum