let S be non empty non void ManySortedSign ; :: thesis: for V being V5 ManySortedSet of the carrier of S
for X1, X2 being SetWithCompoundTerm of S,V
for A being non-empty MSAlgebra of S holds (X1 \/ X2) -Circuit A = (X1 -Circuit A) +* (X2 -Circuit A)
let V be V5 ManySortedSet of the carrier of S; :: thesis: for X1, X2 being SetWithCompoundTerm of S,V
for A being non-empty MSAlgebra of S holds (X1 \/ X2) -Circuit A = (X1 -Circuit A) +* (X2 -Circuit A)
let X1, X2 be SetWithCompoundTerm of S,V; :: thesis: for A being non-empty MSAlgebra of S holds (X1 \/ X2) -Circuit A = (X1 -Circuit A) +* (X2 -Circuit A)
consider t1 being CompoundTerm of S,V such that
A1: t1 in X1 by MSATERM:def 7;
t1 in X1 \/ X2 by A1, XBOOLE_0:def 3;
then reconsider X = X1 \/ X2 as SetWithCompoundTerm of S,V by MSATERM:def 7;
let A be non-empty MSAlgebra of S; :: thesis: (X1 \/ X2) -Circuit A = (X1 -Circuit A) +* (X2 -Circuit A)
set C1 = X1 -Circuit A;
set C2 = X2 -Circuit A;
set C = X -Circuit A;
X1 -Circuit A tolerates X2 -Circuit A by Th19;
then A2: ( the Sorts of (X1 -Circuit A) tolerates the Sorts of (X2 -Circuit A) & the Charact of (X1 -Circuit A) tolerates the Charact of (X2 -Circuit A) ) by CIRCCOMB:def 3;
then A3: ( the Sorts of ((X1 -Circuit A) +* (X2 -Circuit A)) = the Sorts of (X1 -Circuit A) +* the Sorts of (X2 -Circuit A) & the Charact of ((X1 -Circuit A) +* (X2 -Circuit A)) = the Charact of (X1 -Circuit A) +* the Charact of (X2 -Circuit A) ) by CIRCCOMB:def 4;
A4: X -CircuitStr = (X1 -CircuitStr ) +* (X2 -CircuitStr ) by Th11;
( X1 -Circuit A tolerates X -Circuit A & X2 -Circuit A tolerates X -Circuit A ) by Th19;
then A5: ( the Sorts of (X1 -Circuit A) tolerates the Sorts of (X -Circuit A) & the Sorts of (X2 -Circuit A) tolerates the Sorts of (X -Circuit A) & the Charact of (X1 -Circuit A) tolerates the Charact of (X -Circuit A) & the Charact of (X2 -Circuit A) tolerates the Charact of (X -Circuit A) ) by CIRCCOMB:def 3;
( dom the Sorts of ((X1 -Circuit A) +* (X2 -Circuit A)) = the carrier of (X -CircuitStr ) & dom the Charact of ((X1 -Circuit A) +* (X2 -Circuit A)) = the carrier' of (X -CircuitStr ) ) by A4, PBOOLE:def 3;
then ( dom the Charact of ((X1 -Circuit A) +* (X2 -Circuit A)) = dom the Charact of (X -Circuit A) & dom the Sorts of ((X1 -Circuit A) +* (X2 -Circuit A)) = dom the Sorts of (X -Circuit A) ) by PBOOLE:def 3;
then ( the Charact of ((X1 -Circuit A) +* (X2 -Circuit A)) = the Charact of (X -Circuit A) & the Sorts of ((X1 -Circuit A) +* (X2 -Circuit A)) = the Sorts of (X -Circuit A) ) by A2, A3, A5, CIRCCOMB:5, PARTFUN1:136;
hence (X1 \/ X2) -Circuit A = (X1 -Circuit A) +* (X2 -Circuit A) ; :: thesis: verum