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

now

let n be Element of NAT ; :: thesis: (seq2 /" (seq /" seq1)) . n = ((seq2 (#) seq1) /" seq) . n
thus (seq2 /" (seq /" seq1)) . n = (seq2 (#) (seq1 /" seq)) . n by A1, A2, Th37
.= ((seq2 (#) seq1) (#) (seq " )) . n by Th11
.= ((seq2 (#) seq1) /" seq) . n ; :: thesis: verum

end;

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