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