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