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

now :: thesis: for r1, r2 being Element of REAL holds diffreal . (r1,r2) = (addreal * ((id REAL),compreal)) . (r1,r2)

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

end;

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