reconsider ab = [a,b] as Element of [:A,B:] by ZFMISC_1:def 2;
f . ab is Element of C ;
hence f . a,b is Element of C ; :: thesis: verum