let x be Element of 1; :: thesis: Empty^2-to-zero . x,x = 0
[x,x] in [:1,1:] ;
hence Empty^2-to-zero . x,x = 0 by CARD_1:87, FUNCT_2:65; :: thesis: verum