let v, w be Function of [: the carrier of L,(Funcs (X, the carrier of L)):],(Funcs (X, the carrier of L)); :: thesis: ( ( for f being Function of X,L
for a being Element of L holds v . (a,f) = a '*' f ) & ( for f being Function of X,L
for a being Element of L holds w . (a,f) = a '*' f ) implies v = w )
assume that
A1: for f being Function of X,L
for a being Element of L holds v . (a,f) = a '*' f and
A2: for f being Function of X,L
for a being Element of L holds w . (a,f) = a '*' f ; :: thesis: v = w

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

let o be object ; :: thesis: ( o in [: the carrier of L,(Funcs (X, the carrier of L)):] implies v . o = w . o )
assume o in [: the carrier of L,(Funcs (X, the carrier of L)):] ; :: thesis: v . o = w . o
then consider a, h being object such that
A3: ( a in the carrier of L & h in Funcs (X, the carrier of L) & o = [a,h] ) by ZFMISC_1:def 2;
reconsider a = a as Element of the carrier of L by A3;
reconsider h = h as Element of Funcs (X, the carrier of L) by A3;
v . (a,h) = a '*' h by A1
.= w . (a,h) by A2 ;
hence v . o = w . o by A3; :: thesis: verum

end;

hence v = w by FUNCT_2:12; :: thesis: verum