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

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