let r be real number ; :: thesis: for seq1, seq being Real_Sequence holds r (#) (seq1 /" seq) = (r (#) seq1) /" seq
let seq1, seq be Real_Sequence; :: thesis: r (#) (seq1 /" seq) = (r (#) seq1) /" seq
thus r (#) (seq1 /" seq) = r (#) (seq1 (#) (seq "))
.= (r (#) seq1) /" seq by Th26 ; :: thesis: verum