theorem Th10: :: CIRCTRM1:10
for S being non empty non void ManySortedSign
for V being non-empty ManySortedSet of the carrier of S
for X1, X2 being non empty Subset of (S -Terms V) holds (X1 \/ X2) -CircuitStr = (X1 -CircuitStr) +* (X2 -CircuitStr)