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 holds dom s = the carrier of IIG
let SCS be non-empty Circuit of IIG; :: thesis: for s being State of SCS holds dom s = the carrier of IIG
let s be State of SCS; :: thesis: dom s = the carrier of IIG
consider g being Function such that
A1: ( 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 dom s = the carrier of IIG by A1, PBOOLE:def 3; :: thesis: verum