let f1, f2 be Function of (dom F),D; :: thesis: ( ( for x being object st x in dom F holds
f1 . x = B "**" (F . x) ) & ( for x being object st x in dom F holds
f2 . x = B "**" (F . x) ) implies f1 = f2 )
assume that
A4: for x being object st x in dom F holds
f1 . x = B "**" (F . x) and
A5: for x being object st x in dom F holds
f2 . x = B "**" (F . x) ; :: thesis: f1 = f2

now :: thesis: for x being object st x in dom F holds
f1 . x = f2 . x

let x be object ; :: thesis: ( x in dom F implies f1 . x = f2 . x )
assume A6: x in dom F ; :: thesis: f1 . x = f2 . x
hence f1 . x = B "**" (F . x) by A4
.= f2 . x by A5, A6 ;
:: thesis: verum

end;

hence f1 = f2 by FUNCT_2:12; :: thesis: verum