let IIG be non empty non void Circuit-like ManySortedSign ; :: thesis: 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
let SCS be non-empty Circuit of IIG; :: thesis: for InpFs being InputFuncs of SCS
for n being Nat st IIG is with_input_V holds
(commute InpFs) . n is InputValues of SCS
let InpFs be InputFuncs of SCS; :: thesis: for n being Nat st IIG is with_input_V holds
(commute InpFs) . n is InputValues of SCS
let n be Nat; :: thesis: ( IIG is with_input_V implies (commute InpFs) . n is InputValues of SCS )
reconsider A = InputVertices IIG as Subset of IIG ;
reconsider SS = the Sorts of SCS as non-empty ManySortedSet of the carrier of IIG ;
assume IIG is with_input_V ; :: thesis: (commute InpFs) . n is InputValues of SCS
then reconsider A = A as non empty Subset of IIG ;
reconsider SI = SS | A as ManySortedSet of A ;
reconsider SI = SI as non-empty ManySortedSet of A ;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
consider ivm being ManySortedSet of A such that
A1: ivm = (commute InpFs) . n and
A2: ivm in SI by PRE_CIRC:7;

now :: thesis: for v being Vertex of IIG st v in InputVertices IIG holds
ivm . v in the Sorts of SCS . v

let v be Vertex of IIG; :: thesis: ( v in InputVertices IIG implies ivm . v in the Sorts of SCS . v )
assume A3: v in InputVertices IIG ; :: thesis: ivm . v in the Sorts of SCS . v
then SI . v = the Sorts of SCS . v by FUNCT_1:49;
hence ivm . v in the Sorts of SCS . v by A2, A3, PBOOLE:def 1; :: thesis: verum

end;

hence (commute InpFs) . n is InputValues of SCS by A1, MSAFREE2:def 5; :: thesis: verum