let X be non empty finite set ; :: thesis: for S1, S2 being Signature of X
for A1 being Circuit of X,S1
for A2 being Circuit of X,S2 holds A1 +* A2 is gate`2=den
let S1, S2 be Signature of X; :: thesis: for A1 being Circuit of X,S1
for A2 being Circuit of X,S2 holds A1 +* A2 is gate`2=den
A1: the carrier' of (S1 +* S2) = the carrier' of S1 \/ the carrier' of S2 by CIRCCOMB:def 2;
let A1 be Circuit of X,S1; :: thesis: for A2 being Circuit of X,S2 holds A1 +* A2 is gate`2=den
let A2 be Circuit of X,S2; :: thesis: A1 +* A2 is gate`2=den
A2: ( dom the Charact of A1 = the carrier' of S1 & dom the Charact of A2 = the carrier' of S2 ) by PARTFUN1:def 2;
A3: A1 tolerates A2 by Th27;
then the Sorts of A1 tolerates the Sorts of A2 ;
then A4: the Charact of (A1 +* A2) = the Charact of A1 +* the Charact of A2 by CIRCCOMB:def 4;
A5: the Charact of A1 tolerates the Charact of A2 by A3;
A1 +* A2 is gate`2=den hence A1 +* A2 is gate`2=den ; :: thesis: verum