let it1, it2 be BinOp of (Funcs X,the carrier of Y); :: thesis: ( ( for f, g being Element of Funcs X,the carrier of Y holds it1 . f,g = the addF of Y .: f,g ) & ( for f, g being Element of Funcs X,the carrier of Y holds it2 . f,g = the addF of Y .: f,g ) implies it1 = it2 )
assume that
A1: for f, g being Element of Funcs X,the carrier of Y holds it1 . f,g = the addF of Y .: f,g and
A2: for f, g being Element of Funcs X,the carrier of Y holds it2 . f,g = the addF of Y .: f,g ; :: thesis: it1 = it2

now

let f, g be Element of Funcs X,the carrier of Y; :: thesis: it1 . f,g = it2 . f,g
thus it1 . f,g = the addF of Y .: f,g by A1
.= it2 . f,g by A2 ; :: thesis: verum

end;

hence it1 = it2 by BINOP_1:2; :: thesis: verum