let IT be Function of A,C; :: thesis: ( IT = pr2 f iff for x being Element of A holds IT . x = (f . x) `2 )
A14: dom (pr2 f) = dom f by MCART_1:def 13;
then A15: dom (pr2 f) = A by Def1;
hence ( IT = pr2 f implies for x being Element of A holds IT . x = (f . x) `2 ) by A14, MCART_1:def 13; :: thesis: ( ( for x being Element of A holds IT . x = (f . x) `2 ) implies IT = pr2 f )
assume for x being Element of A holds IT . x = (f . x) `2 ; :: thesis: IT = pr2 f
then A16: for x being set st x in dom f holds
IT . x = (f . x) `2 ;
dom IT = dom f by A14, A15, Def1;
hence IT = pr2 f by A16, MCART_1:def 13; :: thesis: verum