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