let a, b be real number ; :: thesis: multreal . a,b = a * b
reconsider a' = a, b' = b as Element of REAL by XREAL_0:def 1;
multreal . a',b' = a' * b' by BINOP_2:def 11;
hence multreal . a,b = a * b ; :: thesis: verum