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