let seq, seq1, seq2 be Complex_Sequence; :: thesis: seq2 /" (seq /" seq1) = (seq2 (#) seq1) /" seq

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

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 Th33
.= ((seq2 (#) seq1) (#) (seq ")) . n by Th8
.= ((seq2 (#) seq1) /" seq) . n ; :: thesis: verum

end;

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