let f, g be Function of (dom F),the carrier of L; :: thesis: ( ( for x being set st x in dom F holds
f . x = \\/ (F . x),L ) & ( for x being set st x in dom F holds
g . x = \\/ (F . x),L ) implies f = g )
assume that
A5: for x being set st x in dom F holds
f . x = \\/ (F . x),L and
A6: for x being set st x in dom F holds
g . x = \\/ (F . x),L ; :: thesis: f = g
A7: ( dom f = dom F & dom g = dom F ) by FUNCT_2:def 1;

now

let x be set ; :: thesis: ( x in dom F implies f . x = g . x )
assume A8: x in dom F ; :: thesis: f . x = g . x
hence f . x = \\/ (F . x),L by A5
.= g . x by A6, A8 ;
:: thesis: verum

end;

hence f = g by A7, FUNCT_1:9; :: thesis: verum