let x, y, c be set ; :: thesis: for f being Function of (2 -tuples_on BOOLEAN ),BOOLEAN holds
( x in the carrier of (2GatesCircStr x,y,c,f) & y in the carrier of (2GatesCircStr x,y,c,f) & c in the carrier of (2GatesCircStr x,y,c,f) )
let f be Function of (2 -tuples_on BOOLEAN ),BOOLEAN ; :: thesis: ( x in the carrier of (2GatesCircStr x,y,c,f) & y in the carrier of (2GatesCircStr x,y,c,f) & c in the carrier of (2GatesCircStr x,y,c,f) )
set S1 = 1GateCircStr <*x,y*>,f;
set S2 = 1GateCircStr <*[<*x,y*>,f],c*>,f;
A1: c in the carrier of (1GateCircStr <*[<*x,y*>,f],c*>,f) by Th43;
( x in the carrier of (1GateCircStr <*x,y*>,f) & y in the carrier of (1GateCircStr <*x,y*>,f) ) by Th43;
hence ( x in the carrier of (2GatesCircStr x,y,c,f) & y in the carrier of (2GatesCircStr x,y,c,f) & c in the carrier of (2GatesCircStr x,y,c,f) ) by A1, Th20; :: thesis: verum