set X = the carrier of AFV;
let o1, o2 be BinOp of the carrier of AFV; :: thesis: ( ( 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) ; :: thesis: o1 = o2
for x being Element of [: the carrier of AFV, the carrier of AFV:] holds o1 . x = o2 . x

proof

let x be Element of [: the carrier of AFV, the carrier of AFV:]; :: thesis: o1 . x = o2 . x
consider x1, x2 being Element of the carrier of AFV such that
A4: x = [x1,x2] by DOMAIN_1:1;
o1 . x = o1 . (x1,x2) by A4
.= Padd (o,x1,x2) by A2
.= o2 . (x1,x2) by A3
.= o2 . x by A4 ;
hence o1 . x = o2 . x ; :: thesis: verum

end;

hence o1 = o2 by FUNCT_2:63; :: thesis: verum