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