let N be non empty SubStr of <REAL,*> ; :: thesis: for a, b being Element of
for x, y being Real st a = x & b = y holds
a * b = x * y
let a, b be Element of ; :: 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 a' = a, b' = b as Element of by TARSKI:def 3;
a * b = a' * b' 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