theorem Th25: :: FACIRC_1:25

for S1, S2, S3 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign
for A1 being Boolean Circuit of S1
for A2 being Boolean Circuit of S2
for A3 being Boolean Circuit of S3 holds (A1 +* A2) +* A3 = A1 +* (A2 +* A3)