let g be Functional of V; :: thesis: ( g = f *' iff for v being Vector of V holds g . v = (f . v) *' )

A2: dom g = the carrier of V by FUNCT_2:def 1;

hence ( g = f *' implies for v being Vector of V holds g . v = (f . v) *' ) by COMSEQ_2:def 1; :: thesis: ( ( for v being Vector of V holds g . v = (f . v) *' ) implies g = f *' )

assume for v being Vector of V holds g . v = (f . v) *' ; :: thesis: g = f *'

then A3: for c being set st c in dom g holds

g . c = (f . c) *' ;

dom f = the carrier of V by FUNCT_2:def 1;

hence g = f *' by A2, A3, COMSEQ_2:def 1; :: thesis: verum

A2: dom g = the carrier of V by FUNCT_2:def 1;

hence ( g = f *' implies for v being Vector of V holds g . v = (f . v) *' ) by COMSEQ_2:def 1; :: thesis: ( ( for v being Vector of V holds g . v = (f . v) *' ) implies g = f *' )

assume for v being Vector of V holds g . v = (f . v) *' ; :: thesis: g = f *'

then A3: for c being set st c in dom g holds

g . c = (f . c) *' ;

dom f = the carrier of V by FUNCT_2:def 1;

hence g = f *' by A2, A3, COMSEQ_2:def 1; :: thesis: verum