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

now

per cases ( ex a, b being Real st
( x = a & y = b & x * y = a * b ) or ( ( x = 0. or y = 0. ) & x * y = 0. ) ) by A1, Def1;

suppose ex a, b being Real st
( x = a & y = b & x * y = a * b ) ; :: thesis: x * y = a * b

then consider a1, b1 being Real such that
A2: ( x = a1 & y = b1 & x * y = a1 * b1 ) ;
thus x * y = a * b by A1, A2; :: thesis: verum

end;

suppose ( ( x = 0. or y = 0. ) & x * y = 0. ) ; :: thesis: x * y = a * b

hence x * y = a * b by A1; :: thesis: verum

end;

end;

end;

hence x * y = a * b ; :: thesis: verum