let HPS be Heptatonic_Pythagorean_Score; :: thesis: for frequency being Element of HPS holds (heptatonic_pythagorean_scale (HPS,frequency)) . 8 = (heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 1
let frequency be Element of HPS; :: thesis: (heptatonic_pythagorean_scale (HPS,frequency)) . 8 = (heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 1
( (heptatonic_pythagorean_scale (HPS,frequency)) . 8 = 2 * (@ frequency) & (heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 1 = 2 * (@ frequency) ) by Th88, Th91;
hence (heptatonic_pythagorean_scale (HPS,frequency)) . 8 = (heptatonic_pythagorean_scale_ascending (HPS,frequency)) . 1 ; :: thesis: verum