let IT be PartFunc 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 A1: IT = f *' ; :: thesis: ( dom IT = C & ( for c being Element of C holds IT . c = (f . c) *' ) )
hence A2: dom IT = dom f by Def1
.= 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) *'
f . c = f /. c ;
hence IT . c = (f . c) *' by A1, A2, Def1; :: thesis: verum

end;

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