theorem :: FACIRC_1:54

for x, y, z being object
for f being Function of (3 -tuples_on BOOLEAN),BOOLEAN
for s being State of (1GateCircuit (x,y,z,f)) holds
( (Following s) . [<*x,y,z*>,f] = f . <*(s . x),(s . y),(s . z)*> & (Following s) . x = s . x & (Following s) . y = s . y & (Following s) . z = s . z ) by Th52;