deffunc H₁( Vertex of ) -> set = the_sort_of $1,A;
thus ex f being ManySortedSet of the carrier of (X -CircuitStr ) st
for d being Element of holds f . d = H₁(d) from PBOOLE:sch 5(); :: thesis: verum