[:2,2:] --> (In (0,REAL)) is Function of [:2,2:],REAL ;
hence [:2,2:] --> 0 is Function of [:2,2:],REAL ; :: thesis: verum