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 Circuit of S1 +* S2
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 Circuit of S1 +* S2
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 Circuit of S1 +* S2
let A2 be Circuit of X,S2; :: thesis: A1 +* A2 is Circuit of S1 +* S2
A1 tolerates A2 by Th30;
then A2: the Sorts of A1 tolerates the Sorts of A2 by CIRCCOMB:def 3;
then A3: the Sorts of (A1 +* A2) = the Sorts of A1 +* the Sorts of A2 by CIRCCOMB:def 4;
A4: ( dom the Sorts of A1 = the carrier of S1 & dom the Sorts of A2 = the carrier of S2 ) by PBOOLE:def 3;
A5: ( the Sorts of A1 is locally-finite & the Sorts of A2 is locally-finite ) by MSAFREE2:def 11;
A1 +* A2 is locally-finite

proof

let i be set ; :: according to PRE_CIRC:def 3,MSAFREE2:def 11 :: thesis: ( not i in the carrier of (S1 +* S2) or the Sorts of (A1 +* A2) . i is finite )
assume i in the carrier of (S1 +* S2) ; :: thesis: the Sorts of (A1 +* A2) . i is finite
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 Sorts of (A1 +* A2) . i = the Sorts of A1 . i ) or ( i in the carrier of S2 & the Sorts of (A1 +* A2) . i = the Sorts of A2 . i ) ) by A2, A3, A4, FUNCT_4:14, FUNCT_4:16;
hence the Sorts of (A1 +* A2) . i is finite by A5, PRE_CIRC:def 3; :: thesis: verum

end;

hence A1 +* A2 is Circuit of S1 +* S2 ; :: thesis: verum