let S be non empty non void ManySortedSign ; 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; 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; 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; (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 Th19;
then A3:
the Sorts of (X1 -Circuit A) tolerates the Sorts of (X2 -Circuit A)
by CIRCCOMB:def 3;
A4:
the Charact of (X1 -Circuit A) tolerates the Charact of (X2 -Circuit A)
by A2, CIRCCOMB:def 3;
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 Th11;
A8:
X1 -Circuit A tolerates X -Circuit A
by Th19;
A9:
X2 -Circuit A tolerates X -Circuit A
by Th19;
A10:
the Sorts of (X1 -Circuit A) tolerates the Sorts of (X -Circuit A)
by A8, CIRCCOMB:def 3;
A11:
the Sorts of (X2 -Circuit A) tolerates the Sorts of (X -Circuit A)
by A9, CIRCCOMB:def 3;
A12:
the Charact of (X1 -Circuit A) tolerates the Charact of (X -Circuit A)
by A8, CIRCCOMB:def 3;
A13:
the Charact of (X2 -Circuit A) tolerates the Charact of (X -Circuit A)
by A9, CIRCCOMB:def 3;
A14:
dom the Sorts of ((X1 -Circuit A) +* (X2 -Circuit A)) = the carrier of (X -CircuitStr )
by A7, PARTFUN1:def 4;
dom the Charact of ((X1 -Circuit A) +* (X2 -Circuit A)) = the carrier' of (X -CircuitStr )
by A7, PARTFUN1:def 4;
then A15:
dom the Charact of ((X1 -Circuit A) +* (X2 -Circuit A)) = dom the Charact of (X -Circuit A)
by PARTFUN1:def 4;
A16:
dom the Sorts of ((X1 -Circuit A) +* (X2 -Circuit A)) = dom the Sorts of (X -Circuit A)
by A14, PARTFUN1:def 4;
A17:
the Charact of ((X1 -Circuit A) +* (X2 -Circuit A)) = the Charact of (X -Circuit A)
by A4, A6, A12, A13, A15, CIRCCOMB:5, PARTFUN1:136;
the Sorts of ((X1 -Circuit A) +* (X2 -Circuit A)) = the Sorts of (X -Circuit A)
by A3, A5, A10, A11, A16, CIRCCOMB:5, PARTFUN1:136;
hence
(X1 \/ X2) -Circuit A = (X1 -Circuit A) +* (X2 -Circuit A)
by A17; verum