deffunc H1( Element of 1 -tuples_on F2()) -> Element of F2() = F3(($1 . 1));
consider g being Function of (1 -tuples_on F2()),F2() such that
A1: for a being Element of 1 -tuples_on F2() holds g . a = H1(a) from FUNCT_2:sch 4();
 reconsider S = 1GateCircStr (<*F1()*>,g) as one-gate ManySortedSign ;
take S ; :: thesis: ex A being one-gate Circuit of S st
( InputVertices S = {F1()} & ( for s being State of A holds (Result s) . (Output S) = F3((s . F1())) ) )
reconsider A = 1GateCircuit (<*F1()*>,g) as one-gate Circuit of S ;
take A ; :: thesis: ( InputVertices S = {F1()} & ( for s being State of A holds (Result s) . (Output S) = F3((s . F1())) ) )
rng <*F1()*> = {F1()} by FINSEQ_1:38;
hence InputVertices S = {F1()} by CIRCCOMB:42; :: thesis: for s being State of A holds (Result s) . (Output S) = F3((s . F1()))
let s be State of A; :: thesis: (Result s) . (Output S) = F3((s . F1()))
reconsider sx = s * <*F1()*> as Element of 1 -tuples_on F2() by Th12;
dom <*F1()*> = Seg 1 by FINSEQ_1:38;
then A2: 1 in dom <*F1()*> by FINSEQ_1:1;
thus (Result s) . (Output S) = (Following s) . (Output S) by Th20
.= (Following s) . [<*F1()*>,g] by Th15
.= g . (s * <*F1()*>) by CIRCCOMB:56
.= F3((sx . 1)) by A1
.= F3((s . (<*F1()*> . 1))) by A2, FUNCT_1:13
.= F3((s . F1())) by FINSEQ_1:def 8 ; :: thesis: verum