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