theorem :: CIRCTRM1:19

for S being non empty non void ManySortedSign
for V being V2() 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)