let seq, seq1 be Complex_Sequence; :: thesis: ( seq is non-zero implies (seq1 /" seq) (#) seq = seq1 )
assume A1: seq is non-zero ; :: thesis: (seq1 /" seq) (#) seq = seq1

now :: thesis: for n being Element of NAT holds ((seq1 /" seq) (#) seq) . n = seq1 . n

let n be Element of NAT ; :: thesis: ((seq1 /" seq) (#) seq) . n = seq1 . n
A2: seq . n <> 0c by A1, Th4;
thus ((seq1 /" seq) (#) seq) . n = ((seq1 (#) (seq ")) . n) * (seq . n) by VALUED_1:5
.= ((seq1 . n) * ((seq ") . n)) * (seq . n) by VALUED_1:5
.= ((seq1 . n) * ((seq . n) ")) * (seq . n) by VALUED_1:10
.= (seq1 . n) * (((seq . n) ") * (seq . n))
.= (seq1 . n) * 1r by A2, XCMPLX_0:def 7
.= seq1 . n ; :: thesis: verum

end;

hence (seq1 /" seq) (#) seq = seq1 by FUNCT_2:63; :: thesis: verum