theorem Th52: :: CIRCCOMB:52

for n being Nat
for X being non empty set
for f being Function of (n -tuples_on X),X
for p being FinSeqLen of n holds
( 1GateCircuit (p,f) is gate`2=den & 1GateCircStr (p,f) is gate`2=den )