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