let UN be Universe; :: thesis: for x, y, z being Element of UN holds (x,y) .--> z is Element of UN
let x, y, z be Element of UN; :: thesis: (x,y) .--> z is Element of UN
(x,y) .--> z = [:{[x,y]},{z}:] ;
hence (x,y) .--> z is Element of UN ; :: thesis: verum