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 V39() 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 ;