thus ex f being ManySortedFunction of V, the Sorts of A st
for x being Element of S
for v being Element of V . x holds S₁[x,v,(f . x) . v] from CIRCTRM1:sch 1(A1); :: thesis: verum