let b be BinOp of REAL ; :: thesis: ( b = diffreal iff b = addreal * (id REAL ),compreal )

now

let r1, r2 be Element of REAL ; :: thesis: diffreal . r1,r2 = (addreal * (id REAL ),compreal ) . r1,r2
thus diffreal . r1,r2 = r1 - r2 by BINOP_2:def 10
.= r1 + (- r2)
.= addreal . r1,(- r2) by BINOP_2:def 9
.= addreal . r1,(compreal . r2) by BINOP_2:def 7
.= (addreal * (id REAL ),compreal ) . r1,r2 by FINSEQOP:87 ; :: thesis: verum

end;

hence ( b = diffreal iff b = addreal * (id REAL ),compreal ) by BINOP_1:2; :: thesis: verum