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