let S be non empty non void ManySortedSign ; for V being non-empty ManySortedSet of the carrier of S
for X1, X2 being SetWithCompoundTerm of S,V
for A being non-empty MSAlgebra over S holds (X1 \/ X2) -Circuit A = (X1 -Circuit A) +* (X2 -Circuit A)
let V be non-empty ManySortedSet of the carrier of S; for X1, X2 being SetWithCompoundTerm of S,V
for A being non-empty MSAlgebra over S holds (X1 \/ X2) -Circuit A = (X1 -Circuit A) +* (X2 -Circuit A)
let X1, X2 be SetWithCompoundTerm of S,V; for A being non-empty MSAlgebra over 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 over S; (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;
A2:
X1 -Circuit A tolerates X2 -Circuit A
by Th18;
then A3:
the Sorts of (X1 -Circuit A) tolerates the Sorts of (X2 -Circuit A)
;
A4:
the Charact of (X1 -Circuit A) tolerates the Charact of (X2 -Circuit A)
by A2;
A5:
the Sorts of ((X1 -Circuit A) +* (X2 -Circuit A)) = the Sorts of (X1 -Circuit A) +* the Sorts of (X2 -Circuit A)
by A3, CIRCCOMB:def 4;
A6:
the Charact of ((X1 -Circuit A) +* (X2 -Circuit A)) = the Charact of (X1 -Circuit A) +* the Charact of (X2 -Circuit A)
by A3, CIRCCOMB:def 4;
A7:
X -CircuitStr = (X1 -CircuitStr) +* (X2 -CircuitStr)
by Th10;
A8:
X1 -Circuit A tolerates X -Circuit A
by Th18;
A9:
X2 -Circuit A tolerates X -Circuit A
by Th18;
A10:
the Sorts of (X1 -Circuit A) tolerates the Sorts of (X -Circuit A)
by A8;
A11:
the Sorts of (X2 -Circuit A) tolerates the Sorts of (X -Circuit A)
by A9;
A12:
the Charact of (X1 -Circuit A) tolerates the Charact of (X -Circuit A)
by A8;
A13:
the Charact of (X2 -Circuit A) tolerates the Charact of (X -Circuit A)
by A9;
A14:
dom the Sorts of ((X1 -Circuit A) +* (X2 -Circuit A)) = the carrier of (X -CircuitStr)
by A7, PARTFUN1:def 2;
dom the Charact of ((X1 -Circuit A) +* (X2 -Circuit A)) = the carrier' of (X -CircuitStr)
by A7, PARTFUN1:def 2;
then A15:
dom the Charact of ((X1 -Circuit A) +* (X2 -Circuit A)) = dom the Charact of (X -Circuit A)
by PARTFUN1:def 2;
A16:
dom the Sorts of ((X1 -Circuit A) +* (X2 -Circuit A)) = dom the Sorts of (X -Circuit A)
by A14, PARTFUN1:def 2;
A17:
the Charact of ((X1 -Circuit A) +* (X2 -Circuit A)) = the Charact of (X -Circuit A)
by A4, A6, A12, A13, A15, FUNCT_4:125, PARTFUN1:55;
the Sorts of ((X1 -Circuit A) +* (X2 -Circuit A)) = the Sorts of (X -Circuit A)
by A3, A5, A10, A11, A16, FUNCT_4:125, PARTFUN1:55;
hence
(X1 \/ X2) -Circuit A = (X1 -Circuit A) +* (X2 -Circuit A)
by A17; verum