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