let seq, seq1, seq9, seq19 be Complex_Sequence; :: thesis: (seq19 /" seq) /" (seq9 /" seq1) = (seq19 (#) seq1) /" (seq (#) seq9)
thus (seq19 /" seq) /" (seq9 /" seq1) = (seq19 /" seq) (#) ((seq9 ") (#) ((seq1 ") ")) by Th29
.= ((seq19 (#) (seq ")) (#) seq1) (#) (seq9 ") by Th8
.= (seq19 (#) (seq1 (#) (seq "))) (#) (seq9 ") by Th8
.= seq19 (#) ((seq1 (#) (seq ")) (#) (seq9 ")) by Th8
.= seq19 (#) (seq1 (#) ((seq ") (#) (seq9 "))) by Th8
.= (seq19 (#) seq1) (#) ((seq ") (#) (seq9 ")) by Th8
.= (seq19 (#) seq1) /" (seq (#) seq9) by Th29 ; :: thesis: verum