let x, y, z be Element of {{} ,{{} }}; :: thesis: Set_to_zero . x,z <= (Set_to_zero . x,y) + (Set_to_zero . y,z)
A1: Set_to_zero . x,y = 0 by Th40;
Set_to_zero . y,z = 0 by Th40;
hence Set_to_zero . x,z <= (Set_to_zero . x,y) + (Set_to_zero . y,z) by A1, Th40; :: thesis: verum