let w1, w2 be BinOp of (Funcs (X, the carrier of L)); :: thesis: ( ( for f, g being Function of X,L holds w1 . (f,g) = f '+' g ) & ( for f, g being Function of X,L holds w2 . (f,g) = f '+' g ) implies w1 = w2 )
assume that
A1: for f, g being Function of X,L holds w1 . (f,g) = f '+' g and
A2: for f, g being Function of X,L holds w2 . (f,g) = f '+' g ; :: thesis: w1 = w2

now :: thesis: for o being object st o in [:(Funcs (X, the carrier of L)),(Funcs (X, the carrier of L)):] holds
w1 . o = w2 . o

let o be object ; :: thesis: ( o in [:(Funcs (X, the carrier of L)),(Funcs (X, the carrier of L)):] implies w1 . o = w2 . o )
assume o in [:(Funcs (X, the carrier of L)),(Funcs (X, the carrier of L)):] ; :: thesis: w1 . o = w2 . o
then consider u, v being object such that
A3: ( u in Funcs (X, the carrier of L) & v in Funcs (X, the carrier of L) & o = [u,v] ) by ZFMISC_1:def 2;
reconsider u = u, v = v as Function of X, the carrier of L by A3, FUNCT_2:66;
w1 . (u,v) = u '+' v by A1
.= w2 . (u,v) by A2 ;
hence w1 . o = w2 . o by A3; :: thesis: verum

end;

hence w1 = w2 by FUNCT_2:12; :: thesis: verum