let x, y, z be Element of {{} ,{{} }}; :: thesis: Set_to_zero . x,z <= (Set_to_zero . x,y) + (Set_to_zero . y,z)
( Set_to_zero . x,y = 0 & 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 Th40; :: thesis: verum