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