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:66; :: thesis: verum