let seq2, seq, seq1 be Complex_Sequence; :: 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 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