now

let IT1, IT2 be Function of A,B; :: thesis: ( ( for x being Element of A holds
( IT1 . x = (F . x) . x & ( for x being Element of A holds IT2 . x = (F . x) . x ) ) ) implies IT1 = IT2 )
assume A3: for x being Element of A holds
( IT1 . x = (F . x) . x & ( for x being Element of A holds IT2 . x = (F . x) . x ) ) ; :: thesis: IT1 = IT2

now

let x be Element of A; :: thesis: IT1 . x = IT2 . x
( IT1 . x = (F . x) . x & IT2 . x = (F . x) . x ) by A3;
hence IT1 . x = IT2 . x ; :: thesis: verum

end;

hence IT1 = IT2 by FUNCT_2:113; :: thesis: verum

end;

hence for b₁, b₂ being Function of A,B st ( for p being Element of A holds b₁ . p = (F . p) . p ) & ( for p being Element of A holds b₂ . p = (F . p) . p ) holds
b₁ = b₂ ; :: thesis: verum