let o, m, r be set ; :: thesis: (o,m) :-> r is Function of [:{o},{m}:],{r}
dom ((o,m) :-> r) = {[o,m]} by Th19
.= [:{o},{m}:] by ZFMISC_1:29 ;
hence (o,m) :-> r is Function of [:{o},{m}:],{r} by FUNCT_2:def 1; :: thesis: verum