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
ex g being Function st
( 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;
hence dom s = the carrier of IIG by PARTFUN1:def 4; :: thesis: verum