let x, y, c be object ; :: 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

( 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