let f be Function of [:{o},{m}:],{r}; :: thesis: ( f = (o,m) .--> r iff verum )
(o,m) .--> r is Function of [:{o},{m}:],{r} by Lm2;
hence ( f = (o,m) .--> r iff verum ) by FUNCT_2:51; :: thesis: verum