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 Th14;
hence InputVertices S = {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₄()))
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 Th13;
dom <*F₁(),F₂(),F₃(),F₄()*> = Seg 4 by FINSEQ_4:92;
then A2: ( 1 in dom <*F₁(),F₂(),F₃(),F₄()*> & 2 in dom <*F₁(),F₂(),F₃(),F₄()*> & 3 in dom <*F₁(),F₂(),F₃(),F₄()*> & 4 in dom <*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₄()*>,g] by Th16
.= g . (s * <*F₁(),F₂(),F₃(),F₄()*>) by CIRCCOMB:64
.= 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 A2, FUNCT_1:23
.= F₆((s . F₁()),(sx . 2),(sx . 3),(sx . 4)) by FINSEQ_4:91
.= F₆((s . F₁()),(s . (<*F₁(),F₂(),F₃(),F₄()*> . 2)),(sx . 3),(sx . 4)) by A2, FUNCT_1:23
.= F₆((s . F₁()),(s . F₂()),(sx . 3),(sx . 4)) by FINSEQ_4:91
.= F₆((s . F₁()),(s . F₂()),(s . (<*F₁(),F₂(),F₃(),F₄()*> . 3)),(sx . 4)) by A2, FUNCT_1:23
.= F₆((s . F₁()),(s . F₂()),(s . F₃()),(sx . 4)) by FINSEQ_4:91
.= F₆((s . F₁()),(s . F₂()),(s . F₃()),(s . (<*F₁(),F₂(),F₃(),F₄()*> . 4))) by A2, FUNCT_1:23
.= F₆((s . F₁()),(s . F₂()),(s . F₃()),(s . F₄())) by FINSEQ_4:91 ;
:: thesis: verum