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