theorem Th48: :: FACIRC_1:48

for x, y being object
for X being non empty finite set
for f being Function of (2 -tuples_on X),X
for s being State of (1GateCircuit (<*x,y*>,f)) holds
( (Following s) . [<*x,y*>,f] = f . <*(s . x),(s . y)*> & (Following s) . x = s . x & (Following s) . y = s . y )