let IT be Function of A,B; :: thesis: ( IT = pr1 f iff for x being Element of A holds IT . x = (f . x) `1 )
A4: dom (pr1 f) = dom f by MCART_1:def 12;
then A5: dom (pr1 f) = A by Def1;
hence ( IT = pr1 f implies for x being Element of A holds IT . x = (f . x) `1 ) by A4, MCART_1:def 12; :: thesis: ( ( for x being Element of A holds IT . x = (f . x) `1 ) implies IT = pr1 f )
assume for x being Element of A holds IT . x = (f . x) `1 ; :: thesis: IT = pr1 f
then A6: for x being object st x in dom f holds
IT . x = (f . x) `1 ;
dom IT = dom f by A4, A5, Def1;
hence IT = pr1 f by A6, MCART_1:def 12; :: thesis: verum