let x, y be Element of 2; :: thesis: Set_to_zero . (x,y) = Set_to_zero . (y,x)
Set_to_zero . (x,y) = 0 by Th27
.= Set_to_zero . (y,x) by Th27 ;
hence Set_to_zero . (x,y) = Set_to_zero . (y,x) ; :: thesis: verum