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 Element of 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 Element of 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 Element of NAT st IIG is with_input_V holds
(commute InpFs) . n is InputValues of SCS
let n be Element of NAT ; :: thesis: ( IIG is with_input_V implies (commute InpFs) . n is InputValues of SCS )
assume A1: IIG is with_input_V ; :: thesis: (commute InpFs) . n is InputValues of SCS
reconsider A = InputVertices IIG as Subset of IIG ;
reconsider A = A as non empty Subset of IIG by A1;
reconsider SS = the Sorts of SCS as V2 ManySortedSet of the carrier of IIG ;
reconsider SI = SS | A as ManySortedSet of A ;
reconsider SI = SI as V2 ManySortedSet of A ;
consider ivm being ManySortedSet of A such that
A2: ( ivm = (commute InpFs) . n & ivm in SI ) by PRE_CIRC:10;

now

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:72;
hence ivm . v in the Sorts of SCS . v by A2, A3, PBOOLE:def 4; :: thesis: verum

end;

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