let IT be Function of C,COMPLEX; :: thesis: ( IT = f *' iff ( dom IT = C & ( for n being Element of C holds IT . n = (f . n) *' ) ) )
thus ( IT = f *' implies ( dom IT = C & ( for c being Element of C holds IT . c = (f . c) *' ) ) ) :: thesis: ( dom IT = C & ( for n being Element of C holds IT . n = (f . n) *' ) implies IT = f *' )

proof

assume A2: IT = f *' ; :: thesis: ( dom IT = C & ( for c being Element of C holds IT . c = (f . c) *' ) )
thus A3: dom IT = C by FUNCT_2:def 1; :: thesis: for c being Element of C holds IT . c = (f . c) *'
let c be Element of C; :: thesis: IT . c = (f . c) *'
thus IT . c = (f . c) *' by A2, A3, Def1; :: thesis: verum

end;

assume that
A4: dom IT = C and
A5: for c being Element of C holds IT . c = (f . c) *' ; :: thesis: IT = f *'
A6: dom IT = dom f by A4, FUNCT_2:def 1;
for c being set st c in dom IT holds
IT . c = (f . c) *' by A5;
hence IT = f *' by A6, Def1; :: thesis: verum