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

now

let n be Element of NAT ; :: thesis: (seq2 /" seq) . n = ((seq2 (#) seq1) /" (seq (#) seq1)) . n
A3: seq1 . n <> 0c by A2, Th4;
thus (seq2 /" seq) . n = ((seq2 . n) * 1r ) * ((seq " ) . n) by VALUED_1:5
.= ((seq2 . n) * ((seq1 . n) * ((seq1 . n) " ))) * ((seq " ) . n) by A3, 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 A1, A2, Th33
.= ((seq2 (#) seq1) /" (seq (#) seq1)) . n by VALUED_1:5 ; :: thesis: verum

end;

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