set X = the carrier of AFV;
let o1, o2 be BinOp of the carrier of AFV; ( ( for a, b being Element of AFV holds o1 . (a,b) = Padd (o,a,b) ) & ( for a, b being Element of AFV holds o2 . (a,b) = Padd (o,a,b) ) implies o1 = o2 )
assume that
A2:
for a, b being Element of AFV holds o1 . (a,b) = Padd (o,a,b)
and
A3:
for a, b being Element of AFV holds o2 . (a,b) = Padd (o,a,b)
; o1 = o2
for x being Element of [: the carrier of AFV, the carrier of AFV:] holds o1 . x = o2 . x
hence
o1 = o2
by FUNCT_2:63; verum