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:35 ;
hence o,m :-> r is Function of [:{o},{m}:],{r} by FUNCT_2:def 1; :: thesis: verum