theorem Th52: :: CIRCCMB3:52

for x1, x2 being set
for X being non empty finite set
for f being Function of (2 -tuples_on X),X
for S being with_nonpair_inputs Signature of X st ( x1 in the carrier of S or not x1 is pair ) & ( x2 in the carrier of S or not x2 is pair ) holds
S +* (1GateCircStr (<*x1,x2*>,f)) is with_nonpair_inputs