let x, y, z be Element of 1; :: thesis: op2 . x,z <= (op2 . x,y) + (op2 . y,z)
( x = {} & y = {} ) by CARD_1:87, TARSKI:def 1;
hence op2 . x,z <= (op2 . x,y) + (op2 . y,z) by Lm1; :: thesis: verum