let x, y be Element of {{} ,{{} }}; :: thesis: Set_to_zero . x,y = Set_to_zero . y,x
Set_to_zero . x,y = 0 by Th40
.= Set_to_zero . y,x by Th40 ;
hence Set_to_zero . x,y = Set_to_zero . y,x ; :: thesis: verum