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