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 Th14;
hence InputVertices S = {F₁(),F₂(),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₃()),(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 Th12;
A2: dom <*F₁(),F₂(),F₃(),F₄(),F₅()*> = Seg 5 by FINSEQ_1:89;
then A3: 1 in dom <*F₁(),F₂(),F₃(),F₄(),F₅()*> by FINSEQ_1:1;
A4: 5 in dom <*F₁(),F₂(),F₃(),F₄(),F₅()*> by A2, FINSEQ_1:1;
A5: 4 in dom <*F₁(),F₂(),F₃(),F₄(),F₅()*> by A2, FINSEQ_1:1;
A6: 3 in dom <*F₁(),F₂(),F₃(),F₄(),F₅()*> by A2, FINSEQ_1:1;
A7: 2 in dom <*F₁(),F₂(),F₃(),F₄(),F₅()*> by A2, FINSEQ_1:1;
Result s = Following s by Th20;
hence (Result s) . (Output S) = (Following s) . [<*F₁(),F₂(),F₃(),F₄(),F₅()*>,g] by Th15
.= g . (s * <*F₁(),F₂(),F₃(),F₄(),F₅()*>) by CIRCCOMB:56
.= 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 A3, FUNCT_1:13
.= F₇((s . F₁()),(sx . 2),(sx . 3),(sx . 4),(sx . 5))
.= F₇((s . F₁()),(s . (<*F₁(),F₂(),F₃(),F₄(),F₅()*> . 2)),(sx . 3),(sx . 4),(sx . 5)) by A7, FUNCT_1:13
.= F₇((s . F₁()),(s . F₂()),(sx . 3),(sx . 4),(sx . 5))
.= F₇((s . F₁()),(s . F₂()),(s . (<*F₁(),F₂(),F₃(),F₄(),F₅()*> . 3)),(sx . 4),(sx . 5)) by A6, FUNCT_1:13
.= F₇((s . F₁()),(s . F₂()),(s . F₃()),(sx . 4),(sx . 5))
.= F₇((s . F₁()),(s . F₂()),(s . F₃()),(s . (<*F₁(),F₂(),F₃(),F₄(),F₅()*> . 4)),(sx . 5)) by A5, FUNCT_1:13
.= F₇((s . F₁()),(s . F₂()),(s . F₃()),(s . F₄()),(sx . 5))
.= F₇((s . F₁()),(s . F₂()),(s . F₃()),(s . F₄()),(s . (<*F₁(),F₂(),F₃(),F₄(),F₅()*> . 5))) by A4, FUNCT_1:13
.= F₇((s . F₁()),(s . F₂()),(s . F₃()),(s . F₄()),(s . F₅())) ;
:: thesis: verum