let IT be FinSequence of COMPLEX ; :: thesis: ( IT = z *' iff ( len IT = len z & ( for i being Nat st 1 <= i & i <= len z holds
IT . i = (z . i) *' ) ) )
thus ( IT = z *' implies ( len IT = len z & ( for i being Nat st 1 <= i & i <= len z holds
IT . i = (z . i) *' ) ) ) :: thesis: ( len IT = len z & ( for i being Nat st 1 <= i & i <= len z holds
IT . i = (z . i) *' ) implies IT = z *' )

proof

assume A3: IT = z *' ; :: thesis: ( len IT = len z & ( for i being Nat st 1 <= i & i <= len z holds
IT . i = (z . i) *' ) )
then dom IT = dom z by COMSEQ_2:def 1;
hence ( len IT = len z & ( for i being Nat st 1 <= i & i <= len z holds
IT . i = (z . i) *' ) ) by A3, COMSEQ_2:def 1, FINSEQ_3:25, FINSEQ_3:29; :: thesis: verum

end;

assume that
A4: len IT = len z and
A5: for i being Nat st 1 <= i & i <= len z holds
IT . i = (z . i) *' ; :: thesis: IT = z *'
A6: dom IT = dom z by A4, FINSEQ_3:29;

now :: thesis: for i being set st i in dom IT holds
IT . i = (z . i) *'

let i be set ; :: thesis: ( i in dom IT implies IT . i = (z . i) *' )
assume A7: i in dom IT ; :: thesis: IT . i = (z . i) *'
then reconsider j = i as Nat ;
( 1 <= j & j <= len z ) by A4, A7, FINSEQ_3:25;
hence IT . i = (z . i) *' by A5; :: thesis: verum

end;

hence IT = z *' by A6, COMSEQ_2:def 1; :: thesis: verum