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 Th25;
then reconsider a9 = a, b9 = b as Element of <REAL,*> by TARSKI:def 3;
a * b = a9 * b9 by Th27;
hence for x, y being Real st a = x & b = y holds
a * b = x * y by BINOP_2:def 11; :: thesis: verum