let seq be Real_Sequence; :: thesis: 1 (#) seq = seq

now :: thesis: for n being Element of NAT holds (1 (#) seq) . n = seq . n

hence
1 (#) seq = seq
by FUNCT_2:63; :: thesis: verumlet n be Element of NAT ; :: thesis: (1 (#) seq) . n = seq . n

thus (1 (#) seq) . n = 1 * (seq . n) by Th9

.= seq . n ; :: thesis: verum

end;thus (1 (#) seq) . n = 1 * (seq . n) by Th9

.= seq . n ; :: thesis: verum