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