consider A being Circuit of S such that
A1: ( the Sorts of A is constant & the_value_of the Sorts of A = X ) and
A2: A is gate`2=den by Def9;
set B = MSAlgebra(# the Sorts of A,the Charact of A #);
the Sorts of A is finite-yielding by MSAFREE2:def 11;
then reconsider B = MSAlgebra(# the Sorts of A,the Charact of A #) as Circuit of S by MSAFREE2:def 11;
for g being set st g in the carrier' of S holds
g = [(g `1 ),(the Charact of B . g)] by A2, CIRCCOMB:def 10;
then B is gate`2=den by CIRCCOMB:def 10;
then reconsider B = B as Circuit of X,S by A1, Def10;
consider Y being non empty finite set , n being Element of NAT , p being FinSeqLen of n, f being Function of (n -tuples_on Y),Y such that
A3: S = 1GateCircStr p,f by Def6;
take B ; :: thesis: ( B is strict & B is one-gate )
A4: dom the Arity of S = the carrier' of S by FUNCT_2:def 1;
dom the Sorts of A = the carrier of S by PARTFUN1:def 4;
then A5: the Sorts of B = the carrier of S --> X by A1, FUNCOP_1:95;
set g = [p,f];
set C = 1GateCircuit p,f;
[p,f] in {[p,f]} by TARSKI:def 1;
then A6: [p,f] in the carrier' of S by A3, CIRCCOMB:def 6;
then A7: [p,f] = [([p,f] `1 ),(the Charact of (1GateCircuit p,f) . [p,f])] by A3, CIRCCOMB:def 10;
the Arity of S . [p,f] in the carrier of S * by A6, FUNCT_2:7;
then reconsider Ag = the Arity of S . [p,f] as FinSequence of the carrier of S by FINSEQ_1:def 11;
dom the ResultSort of S = the carrier' of S by FUNCT_2:def 1;
then A8: (the Sorts of B * the ResultSort of S) . [p,f] = the Sorts of B . (the ResultSort of S . [p,f]) by A6, FUNCT_1:23;
the ResultSort of S . [p,f] in the carrier of S by A6, FUNCT_2:7;
then the ResultSort of S . [p,f] in dom the Sorts of B by PARTFUN1:def 4;
then A9: the Sorts of B . (the ResultSort of S . [p,f]) = X by A1, FUNCT_1:def 18;
A10: [p,f] = [([p,f] `1 ),(the Charact of B . [p,f])] by A6, CIRCCOMB:def 10;
then dom (the Charact of B . [p,f]) = dom f by ZFMISC_1:33;
then A11: dom (the Charact of B . [p,f]) = n -tuples_on Y by FUNCT_2:def 1;
the Charact of B . [p,f] is Function of (((the Sorts of B # ) * the Arity of S) . [p,f]),((the Sorts of B * the ResultSort of S) . [p,f]) by A6, PBOOLE:def 18;
then dom (the Charact of B . [p,f]) = ((the Sorts of B # ) * the Arity of S) . [p,f] by A6, FUNCT_2:def 1;
then A12: dom (the Charact of B . [p,f]) = (the Sorts of B # ) . Ag by A6, A4, FUNCT_1:23
.= (len Ag) -tuples_on X by A5, CIRCCOMB:6 ;

per cases ( n <> 0 or n = 0 ) ;

suppose A13: n <> 0 ; :: thesis: ( B is strict & B is one-gate )

A14: now

let i be set ; :: thesis: ( i in the carrier' of S implies the Charact of B . i = the Charact of (1GateCircuit p,f) . i )
assume i in the carrier' of S ; :: thesis: the Charact of B . i = the Charact of (1GateCircuit p,f) . i
then i in {[p,f]} by A3, CIRCCOMB:def 6;
then i = [p,f] by TARSKI:def 1;
hence the Charact of B . i = the Charact of (1GateCircuit p,f) . i by A10, A7, ZFMISC_1:33; :: thesis: verum

end;

X = Y by A11, A12, A13, Th24;
then the Sorts of B = the Sorts of (1GateCircuit p,f) by A3, A5, CIRCCOMB:def 14;
hence ( B is strict & B is one-gate ) by A3, A14, PBOOLE:3; :: thesis: verum

end;

suppose A15: n = 0 ; :: thesis: ( B is strict & B is one-gate )

then n -tuples_on X = {(<*> X)} by FINSEQ_2:112
.= {(<*> Y)}
.= n -tuples_on Y by A15, FINSEQ_2:112 ;
then A16: dom f = n -tuples_on X by FUNCT_2:def 1;
the Charact of B . [p,f] is Function of (((the Sorts of B # ) * the Arity of S) . [p,f]),((the Sorts of B * the ResultSort of S) . [p,f]) by A6, PBOOLE:def 18;
then A17: rng (the Charact of B . [p,f]) c= (the Sorts of B * the ResultSort of S) . [p,f] by RELAT_1:def 19;
the Charact of B . [p,f] = f by A10, ZFMISC_1:33;
then reconsider h = f as Function of (n -tuples_on X),X by A8, A9, A17, A16, FUNCT_2:4;
set D = 1GateCircuit p,h;
A18: [p,f] = [([p,f] `1 ),(the Charact of (1GateCircuit p,h) . [p,f])] by A3, A6, CIRCCOMB:def 10;

A19: now

let i be set ; :: thesis: ( i in the carrier' of S implies the Charact of B . i = the Charact of (1GateCircuit p,h) . i )
assume i in the carrier' of S ; :: thesis: the Charact of B . i = the Charact of (1GateCircuit p,h) . i
then i in {[p,f]} by A3, CIRCCOMB:def 6;
then i = [p,f] by TARSKI:def 1;
hence the Charact of B . i = the Charact of (1GateCircuit p,h) . i by A10, A18, ZFMISC_1:33; :: thesis: verum

end;

the Sorts of B = the Sorts of (1GateCircuit p,h) by A3, A5, CIRCCOMB:def 14;
hence ( B is strict & B is one-gate ) by A3, A19, PBOOLE:3; :: thesis: verum

end;

end;