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

now :: thesis: for f, g being Element of Funcs ( the carrier of M, the carrier of N) holds it1 . (f,g) = it2 . (f,g)

let f, g be Element of Funcs ( the carrier of M, the carrier of N); :: thesis: it1 . (f,g) = it2 . (f,g)
thus it1 . (f,g) = the addF of N .: (f,g) by A2
.= it2 . (f,g) by A3 ; :: thesis: verum

end;

hence it1 = it2 ; :: thesis: verum