let x, y be R_eal; :: thesis: for a, b being Real st x = a & y = b holds
x * y = a * b
let a, b be Real; :: thesis: ( x = a & y = b implies x * y = a * b )
assume A1: ( x = a & y = b ) ; :: thesis: x * y = a * b
reconsider a = a, b = b as real number ;
x * y = a * b by A1;
hence x * y = a * b ; :: thesis: verum