let x, y, z be Element of 1; :: thesis: Empty^2-to-zero . x,z <= (Empty^2-to-zero . x,y) + (Empty^2-to-zero . y,z)
A1: z = {} by CARD_1:87, TARSKI:def 1;
x = {} by CARD_1:87, TARSKI:def 1;
then ( y = {} & Empty^2-to-zero . x,z = 0 ) by A1, Th4, CARD_1:87, TARSKI:def 1;
hence Empty^2-to-zero . x,z <= (Empty^2-to-zero . x,y) + (Empty^2-to-zero . y,z) by A1, Th4; :: thesis: verum