g . f in REAL * ;
hence g . f is Element of REAL * ; :: thesis: verum