for IIG being non empty non void Circuit-like ManySortedSign
for SCS being non-empty Circuit of IIG
for InpFs being InputFuncs of SCS
for n being Nat st IIG is with_input_V holds
(commute InpFs) . n is InputValues of SCS