theorem :: GFACIRC1:56

for x, y, z being set holds
( x in the carrier of (GFA1AdderStr (x,y,z)) & y in the carrier of (GFA1AdderStr (x,y,z)) & z in the carrier of (GFA1AdderStr (x,y,z)) & [<*x,y*>,xor2c] in the carrier of (GFA1AdderStr (x,y,z)) & [<*[<*x,y*>,xor2c],z*>,xor2c] in the carrier of (GFA1AdderStr (x,y,z)) ) by FACIRC_1:60, FACIRC_1:61;