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 Th28;
A1: dom the Sorts of A1 = the carrier of S1 by PARTFUN1:def 2;
( the Sorts of A1 is constant & the_value_of the Sorts of A1 = X ) by Def10;
then the Sorts of A1 = (dom the Sorts of A1) --> X by FUNCOP_1:80;
then A2: the Sorts of A1 = [:(dom the Sorts of A1),{X}:] by FUNCOP_1:def 2;
( the Sorts of A2 is constant & the_value_of the Sorts of A2 = X ) by Def10;
then the Sorts of A2 = (dom the Sorts of A2) --> X by FUNCOP_1:80;
then A3: the Sorts of A2 = [:(dom the Sorts of A2),{X}:] by FUNCOP_1:def 2;
A1 tolerates A2 by Th27;
then A4: the Sorts of A1 tolerates the Sorts of A2 ;
then the Sorts of A = the Sorts of A1 +* the Sorts of A2 by CIRCCOMB:def 4
.= the Sorts of A1 \/ the Sorts of A2 by A4, FUNCT_4:30
.= [:((dom the Sorts of A1) \/ (dom the Sorts of A2)),{X}:] by A2, A3, ZFMISC_1:97
.= ( the carrier of S1 \/ (dom the Sorts of A2)) --> X by A1, FUNCOP_1:def 2 ;
hence ( the Sorts of (A1 +* A2) is constant & the_value_of the Sorts of (A1 +* A2) = X ) by FUNCOP_1:79; :: thesis: verum