let IT be Function of C,COMPLEX; :: thesis: ( IT = f *' iff for n being Element of C holds IT . n = (f . n) *' )
A2: dom IT = C by FUNCT_2:def 1;
hence ( IT = f *' implies for c being Element of C holds IT . c = (f . c) *' ) by Def1; :: thesis: ( ( for n being Element of C holds IT . n = (f . n) *' ) implies IT = f *' )
assume A3: for c being Element of C holds IT . c = (f . c) *' ; :: thesis: IT = f *'
A4: dom IT = dom f by A2, FUNCT_2:def 1;
for c being set st c in dom IT holds
IT . c = (f . c) *' by A3;
hence IT = f *' by A4, Def1; :: thesis: verum