assume A1: ( a = c & b = d ) ; :: thesis: a * b = c * d
reconsider a = a, b = b as Element of INT ;
multint . a,b = multreal . a,b by Def1
.= c * d by A1, BINOP_2:def 11 ;
hence a * b = c * d ; :: thesis: verum