theorem Th6: :: CIRCTRM1:6

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
( the Arity of (X1 -CircuitStr) tolerates the Arity of (X2 -CircuitStr) & the ResultSort of (X1 -CircuitStr) tolerates the ResultSort of (X2 -CircuitStr) )