now :: thesis: for IT1, IT2 being Function of A,B st ( for x being Element of A holds

( IT1 . x = (F . x) . x & ( for x being Element of A holds IT2 . x = (F . x) . x ) ) ) holds

IT1 = IT2

hence
for b( IT1 . x = (F . x) . x & ( for x being Element of A holds IT2 . x = (F . x) . x ) ) ) holds

IT1 = IT2

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

end;( 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 :: thesis: for x being Element of A holds IT1 . x = IT2 . x

hence
IT1 = IT2
by FUNCT_2:63; :: thesis: verumlet x be Element of A; :: thesis: IT1 . x = IT2 . x

IT1 . x = (F . x) . x by A3;

hence IT1 . x = IT2 . x by A3; :: thesis: verum

end;IT1 . x = (F . x) . x by A3;

hence IT1 . x = IT2 . x by A3; :: thesis: verum

b