[:f1,f2:] is Function of [:X1,X2:],[:Y1,Y2:] ;
hence [:f1,f2:] is Function of [:X1,X2:],[:Y1,Y2:] ; :: thesis: verum