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
A1: dom the Sorts of SCS = the carrier of IIG by PBOOLE:def 3;
consider g being Function such that
A2: ( s = g & dom g = dom the Sorts of SCS & ( for x being set st x in dom the Sorts of SCS holds
g . x in the Sorts of SCS . x ) ) by CARD_3:def 5;
thus s . v in the Sorts of SCS . v by A1, A2; :: thesis: verum