let S1, S2, S3 be non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign ; :: thesis: 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)
let A1 be Boolean Circuit of S1; :: thesis: for A2 being Boolean Circuit of S2
for A3 being Boolean Circuit of S3 holds (A1 +* A2) +* A3 = A1 +* (A2 +* A3)
let A2 be Boolean Circuit of S2; :: thesis: for A3 being Boolean Circuit of S3 holds (A1 +* A2) +* A3 = A1 +* (A2 +* A3)
let A3 be Boolean Circuit of S3; :: thesis: (A1 +* A2) +* A3 = A1 +* (A2 +* A3)
A1: the Sorts of A3 tolerates the Sorts of A1 by CIRCCOMB:59;
( the Sorts of A1 tolerates the Sorts of A2 & the Sorts of A2 tolerates the Sorts of A3 ) by CIRCCOMB:59;
hence (A1 +* A2) +* A3 = A1 +* (A2 +* A3) by A1, CIRCCOMB:23; :: thesis: verum