let IIG be non empty non void Circuit-like ManySortedSign ; :: thesis: for SCS being non-empty Circuit of IIG
for s being State of SCS
for v being Vertex of IIG holds s . v in the Sorts of SCS . v
let SCS be non-empty Circuit of IIG; :: thesis: for s being State of SCS
for v being Vertex of IIG holds s . v in the Sorts of SCS . v
let s be State of SCS; :: thesis: for v being Vertex of IIG holds s . v in the Sorts of SCS . v
let v be Vertex of IIG; :: thesis: s . v in the Sorts of SCS . v
( dom the Sorts of SCS = the carrier of IIG & ex g being Function st
( s = g & dom g = dom the Sorts of SCS & ( for x being object st x in dom the Sorts of SCS holds
g . x in the Sorts of SCS . x ) ) ) by CARD_3:def 5, PARTFUN1:def 2;
hence s . v in the Sorts of SCS . v ; :: thesis: verum