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 9; :: thesis: verum