let IT be Function of A,C; :: thesis: ( IT = pr2 f iff for x being Element of A holds IT . x = (f . x) `2 )
A10: dom (pr2 f) = dom f by MCART_1:def 13;
then A11: dom (pr2 f) = A by Def1;
hence ( IT = pr2 f implies for x being Element of A holds IT . x = (f . x) `2 ) by A10, 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 A12: for x being object st x in dom f holds
IT . x = (f . x) `2 ;
dom IT = dom f by A10, A11, Def1;
hence IT = pr2 f by A12, MCART_1:def 13; :: thesis: verum