set KK = the carrier of K;
let f1, f2 be Function of [:( the carrier of K *),( the carrier of K *):],( the carrier of K *); :: thesis: ( ( for p1, p2 being Element of the carrier of K * holds f1 . (p1,p2) = p1 + p2 ) & ( for p1, p2 being Element of the carrier of K * holds f2 . (p1,p2) = p1 + p2 ) implies f1 = f2 )
assume that
A3: for p1, p2 being Element of the carrier of K * holds f1 . (p1,p2) = p1 + p2 and
A4: for p1, p2 being Element of the carrier of K * holds f2 . (p1,p2) = p1 + p2 ; :: thesis: f1 = f2

now

let p1, p2 be Element of the carrier of K * ; :: thesis: f1 . (p1,p2) = f2 . (p1,p2)
f1 . (p1,p2) = p1 + p2 by A3;
hence f1 . (p1,p2) = f2 . (p1,p2) by A4; :: thesis: verum

end;

hence f1 = f2 by BINOP_1:2; :: thesis: verum