let seq19, seq, seq9, seq1 be Real_Sequence; :: thesis: (seq19 /" seq) /" (seq9 /" seq1) = (seq19 (#) seq1) /" (seq (#) seq9)
thus (seq19 /" seq) /" (seq9 /" seq1) = (seq19 /" seq) (#) ((seq9 " ) (#) ((seq1 " ) " )) by Th44
.= ((seq19 (#) (seq " )) (#) seq1) (#) (seq9 " ) by Th22
.= (seq19 (#) (seq1 (#) (seq " ))) (#) (seq9 " ) by Th22
.= seq19 (#) ((seq1 (#) (seq " )) (#) (seq9 " )) by Th22
.= seq19 (#) (seq1 (#) ((seq " ) (#) (seq9 " ))) by Th22
.= (seq19 (#) seq1) (#) ((seq " ) (#) (seq9 " )) by Th22
.= (seq19 (#) seq1) /" (seq (#) seq9) by Th44 ; :: thesis: verum