let IIG be non empty finite non void Circuit-like monotonic ManySortedSign ; :: thesis: for SCS being non-empty Circuit of IIG
for InpFs being InputFuncs of SCS st commute InpFs is constant & not InputVertices IIG is empty holds
for s1, s2 being State of SCS holds (Computation s1,InpFs) . (depth SCS) = (Computation s2,InpFs) . (depth SCS)
let SCS be non-empty Circuit of IIG; :: thesis: for InpFs being InputFuncs of SCS st commute InpFs is constant & not InputVertices IIG is empty holds
for s1, s2 being State of SCS holds (Computation s1,InpFs) . (depth SCS) = (Computation s2,InpFs) . (depth SCS)
let InpFs be InputFuncs of SCS; :: thesis: ( commute InpFs is constant & not InputVertices IIG is empty implies for s1, s2 being State of SCS holds (Computation s1,InpFs) . (depth SCS) = (Computation s2,InpFs) . (depth SCS) )
assume A1: ( commute InpFs is constant & not InputVertices IIG is empty ) ; :: thesis: for s1, s2 being State of SCS holds (Computation s1,InpFs) . (depth SCS) = (Computation s2,InpFs) . (depth SCS)
then A2: IIG is with_input_V by MSAFREE2:def 4;
let s1, s2 be State of SCS; :: thesis: (Computation s1,InpFs) . (depth SCS) = (Computation s2,InpFs) . (depth SCS)
reconsider dSCS = depth SCS as Element of NAT by ORDINAL1:def 13;
reconsider Cs1 = (Computation s1,InpFs) . dSCS as State of SCS ;
reconsider Cs2 = (Computation s2,InpFs) . dSCS as State of SCS ;
reconsider iv = (commute InpFs) . 0 as InputValues of SCS by A2, CIRCUIT1:2;

now

thus the carrier of IIG = dom Cs1 by CIRCUIT1:4; :: thesis: ( the carrier of IIG = dom Cs2 & ( for x being set st x in the carrier of IIG holds
Cs1 . x = Cs2 . x ) )
thus the carrier of IIG = dom Cs2 by CIRCUIT1:4; :: thesis: for x being set st x in the carrier of IIG holds
Cs1 . x = Cs2 . x
let x be set ; :: thesis: ( x in the carrier of IIG implies Cs1 . x = Cs2 . x )
assume x in the carrier of IIG ; :: thesis: Cs1 . x = Cs2 . x
then reconsider x' = x as Vertex of IIG ;
( Cs1 . x' = IGValue x',iv & Cs2 . x' = IGValue x',iv ) by A1, Th17;
hence Cs1 . x = Cs2 . x ; :: thesis: verum

end;

hence (Computation s1,InpFs) . (depth SCS) = (Computation s2,InpFs) . (depth SCS) by FUNCT_1:9; :: thesis: verum