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