let x, y be Element of {{} ,{{} }}; :: thesis: Set_to_zero . x,y = 0
thus Set_to_zero . x,y = Set_to_zero . [x,y]
.= 0 by FUNCOP_1:13 ; :: thesis: verum