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