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
A2: ( dom the Sorts of A1 = the carrier of S1 & dom the Sorts of A2 = the carrier of S2 ) by PARTFUN1:def 2;
A3: ( the Sorts of A1 is V39() & the Sorts of A2 is V39() ) by MSAFREE2:def 11;
A1 tolerates A2 by Th27;
then A4: the Sorts of A1 tolerates the Sorts of A2 ;
then A5: the Sorts of (A1 +* A2) = the Sorts of A1 +* the Sorts of A2 by CIRCCOMB:def 4;
A1 +* A2 is finite-yielding
proof
let i be object ; :: according to MSAFREE2:def 11,FINSET_1:def 5 :: 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 A4, A5, A2, FUNCT_4:13, FUNCT_4:15;
hence the Sorts of (A1 +* A2) . i is finite by A3; :: thesis: verum
end;
hence A1 +* A2 is Circuit of S1 +* S2 ; :: thesis: verum