defpred S₁[ object , object , object ] means ex w, u, v being Function of X,L st
( w = $3 & u = $1 & v = $2 & w = u '+' v );
A0: for x, y being object st x in Funcs (X, the carrier of L) & y in Funcs (X, the carrier of L) holds
ex z being object st
( z in Funcs (X, the carrier of L) & S₁[x,y,z] )

proof

let x, y be object ; :: thesis: ( x in Funcs (X, the carrier of L) & y in Funcs (X, the carrier of L) implies ex z being object st
( z in Funcs (X, the carrier of L) & S₁[x,y,z] ) )
assume ( x in Funcs (X, the carrier of L) & y in Funcs (X, the carrier of L) ) ; :: thesis: ex z being object st
( z in Funcs (X, the carrier of L) & S₁[x,y,z] )
then reconsider u = x, v = y as Function of X, the carrier of L by FUNCT_2:66;
take z = u '+' v; :: thesis: ( z in Funcs (X, the carrier of L) & S₁[x,y,z] )
thus z in Funcs (X, the carrier of L) by FUNCT_2:8; :: thesis: S₁[x,y,z]
thus S₁[x,y,z] ; :: thesis: verum

end;

consider h being Function of [:(Funcs (X, the carrier of L)),(Funcs (X, the carrier of L)):],(Funcs (X, the carrier of L)) such that
A1: for x, y being object st x in Funcs (X, the carrier of L) & y in Funcs (X, the carrier of L) holds
S₁[x,y,h . (x,y)] from BINOP_1:sch 1(A0);
take h ; :: thesis: for f, g being Function of X,L holds h . (f,g) = f '+' g

now :: thesis: for f, g being Function of X, the carrier of L holds h . (f,g) = f '+' g

let f, g be Function of X, the carrier of L; :: thesis: h . (f,g) = f '+' g
( f in Funcs (X, the carrier of L) & g in Funcs (X, the carrier of L) ) by FUNCT_2:8;
then S₁[f,g,h . (f,g)] by A1;
hence h . (f,g) = f '+' g ; :: thesis: verum

end;

hence for f, g being Function of X,L holds h . (f,g) = f '+' g ; :: thesis: verum