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
( the Sorts of (A1 +* A2) is constant & the_value_of the Sorts of (A1 +* A2) = X )
let S1, S2 be Signature of X; :: thesis: for A1 being Circuit of X,S1
for A2 being Circuit of X,S2 holds
( the Sorts of (A1 +* A2) is constant & the_value_of the Sorts of (A1 +* A2) = X )
let A1 be Circuit of X,S1; :: thesis: for A2 being Circuit of X,S2 holds
( the Sorts of (A1 +* A2) is constant & the_value_of the Sorts of (A1 +* A2) = X )
let A2 be Circuit of X,S2; :: thesis: ( the Sorts of (A1 +* A2) is constant & the_value_of the Sorts of (A1 +* A2) = X )
reconsider A = A1 +* A2 as Circuit of S1 +* S2 by Th31;
A1 tolerates A2 by Th30;
then A1: the Sorts of A1 tolerates the Sorts of A2 by CIRCCOMB:def 3;
( the Sorts of A1 is constant & the_value_of the Sorts of A1 = X & the Sorts of A2 is constant & the_value_of the Sorts of A2 = X ) by Def10;
then ( the Sorts of A1 = (dom the Sorts of A1) --> X & the Sorts of A2 = (dom the Sorts of A2) --> X ) by FUNCOP_1:95;
then A2: ( the Sorts of A1 = [:(dom the Sorts of A1),{X}:] & the Sorts of A2 = [:(dom the Sorts of A2),{X}:] ) by FUNCOP_1:def 2;
A3: dom the Sorts of A1 = the carrier of S1 by PARTFUN1:def 4;
the Sorts of A = the Sorts of A1 +* the Sorts of A2 by A1, CIRCCOMB:def 4
.= the Sorts of A1 \/ the Sorts of A2 by A1, FUNCT_4:31
.= [:((dom the Sorts of A1) \/ (dom the Sorts of A2)),{X}:] by A2, ZFMISC_1:120
.= (the carrier of S1 \/ (dom the Sorts of A2)) --> X by A3, FUNCOP_1:def 2 ;
hence ( the Sorts of (A1 +* A2) is constant & the_value_of the Sorts of (A1 +* A2) = X ) by FUNCOP_1:94; :: thesis: verum