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 4;
A3: A1 tolerates A2 by Th30;
then the Sorts of A1 tolerates the Sorts of A2 by CIRCCOMB:def 3;
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, CIRCCOMB:def 3;
A1 +* A2 is gate`2=den

proof

let i be set ; :: according to CIRCCOMB:def 10 :: thesis: ( not i in the carrier' of (S1 +* S2) or i = [(i `1),( the Charact of (A1 +* A2) . i)] )
assume i in the carrier' of (S1 +* S2) ; :: thesis: i = [(i `1),( the Charact of (A1 +* A2) . i)]
then ( i in the carrier' of S1 or i in the carrier' of S2 ) by A1, XBOOLE_0:def 3;
then ( ( i in the carrier' of S1 & the Charact of (A1 +* A2) . i = the Charact of A1 . i ) or ( i in the carrier' of S2 & the Charact of (A1 +* A2) . i = the Charact of A2 . i ) ) by A5, A4, A2, FUNCT_4:14, FUNCT_4:16;
hence i = [(i `1),( the Charact of (A1 +* A2) . i)] by CIRCCOMB:def 10; :: thesis: verum

end;

hence A1 +* A2 is gate`2=den ; :: thesis: verum