defpred S₁[ object , object , object ] means ex u, w being Function of X,L ex a being Element of L st
( w = $3 & a = $1 & u = $2 & w = a '*' u );
A0: for x, y being object st x in 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 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 B: ( x in 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 a = x as Element of the carrier of L ;
reconsider h = y as Element of Funcs (X, the carrier of L) by B;
take z = a '*' h; :: 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 [: 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 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 being Function of X,L
for a being Element of L holds h . (a,f) = a '*' f

now :: thesis: for a being Element of L
for f being Function of X,L holds h . (a,f) = a '*' f

let a be Element of L; :: thesis: for f being Function of X,L holds h . (a,f) = a '*' f
let f be Function of X,L; :: thesis: h . (a,f) = a '*' f
f in Funcs (X, the carrier of L) by FUNCT_2:8;
then S₁[a,f,h . (a,f)] by A1;
hence h . (a,f) = a '*' f ; :: thesis: verum

end;

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