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

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