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 *' )

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;

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 that
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;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

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) *'

hence
IT = z *'
by A6, COMSEQ_2:def 1; :: thesis: verumIT . 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;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