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