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;
then B is gate`2=den ;
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 2;
then A5: the Sorts of B = the carrier of S --> X by A1, FUNCOP_1:80;
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:5;
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:13;
the ResultSort of S . [p,f] in the carrier of S by A6, FUNCT_2:5;
then the ResultSort of S . [p,f] in dom the Sorts of B by PARTFUN1:def 2;
then A9: the Sorts of B . ( the ResultSort of S . [p,f]) = X by A1, FUNCT_1:def 12;
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 XTUPLE_0:1;
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 15;
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:13
.= (len Ag) -tuples_on X by A5, CIRCCOMB:2 ;

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

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

A14: now :: thesis: for i being object st i in the carrier' of S holds
the Charact of B . i = the Charact of (1GateCircuit (p,f)) . i

let i be object ; :: 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, XTUPLE_0:1; :: thesis: verum

end;

X = Y by A11, A12, A13, Th22;
then the Sorts of B = the Sorts of (1GateCircuit (p,f)) by A3, A5, CIRCCOMB:def 13;
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:94
.= {(<*> Y)}
.= n -tuples_on Y by A15, FINSEQ_2:94 ;
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 15;
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, XTUPLE_0:1;
then reconsider h = f as Function of (n -tuples_on X),X by A8, A9, A17, A16, FUNCT_2:2;
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 :: thesis: for i being object st i in the carrier' of S holds
the Charact of B . i = the Charact of (1GateCircuit (p,h)) . i

let i be object ; :: 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, XTUPLE_0:1; :: thesis: verum

end;

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

end;

end;