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

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

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

end;

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