thus pr2 (D1,D2) is Function of [:D1,D2:],D2 ; :: thesis: verum