let f, g be Function of (dom F), the carrier of L; :: thesis: ( ( for x being object st x in dom F holds
f . x = //\ ((F . x),L) ) & ( for x being object st x in dom F holds
g . x = //\ ((F . x),L) ) implies f = g )
assume that
A11: for x being object st x in dom F holds
f . x = //\ ((F . x),L) and
A12: for x being object st x in dom F holds
g . x = //\ ((F . x),L) ; :: thesis: f = g

A13: now :: thesis: for x being object st x in dom F holds
f . x = g . x

let x be object ; :: thesis: ( x in dom F implies f . x = g . x )
assume A14: x in dom F ; :: thesis: f . x = g . x
hence f . x = //\ ((F . x),L) by A11
.= g . x by A12, A14 ;
:: thesis: verum

end;

( dom f = dom F & dom g = dom F ) by FUNCT_2:def 1;
hence f = g by A13, FUNCT_1:2; :: thesis: verum