let o, m, r be object ; :: thesis: (o,m) :-> r is Function of [:{o},{m}:],{r}
[:{o},{m}:] = {[o,m]} by ZFMISC_1:29;
hence (o,m) :-> r is Function of [:{o},{m}:],{r} ; :: thesis: verum