0 in REAL ;
then ( op2 is Function of [:1,1:],1 & 1 c= REAL ) by CARD_1:87, ZFMISC_1:37;
hence Empty^2-to-zero is Function of [:1,1:],REAL by FUNCT_2:9; :: thesis: verum