for X being non empty finite set
for S1, S2 being Signature of X
for A1 being Circuit of X,S1
for A2 being Circuit of X,S2 holds
( the Sorts of (A1 +* A2) is constant & the_value_of the Sorts of (A1 +* A2) = X )