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