let N be non empty SubStr of <REAL,*> ; :: thesis: for a, b being Element of N
for x, y being Real st a = x & b = y holds
a * b = x * y
let a, b be Element of N; :: thesis: for x, y being Real st a = x & b = y holds
a * b = x * y
H₁(N) c= H₁( <REAL,*> ) by Th23;
then reconsider a9 = a, b9 = b as Element of <REAL,*> ;
a * b = a9 * b9 by Th25;
hence for x, y being Real st a = x & b = y holds
a * b = x * y by BINOP_2:def 11; :: thesis: verum