let MS be non empty satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed satisfying_fifth_constructible MusicStruct ; for frequency being Element of MS ex seq being sequence of MS st
( seq . 0 = frequency & ( for n being Nat holds [(seq . n),(seq . (n + 1))] in fifth MS ) )
let frequency be Element of MS; ex seq being sequence of MS st
( seq . 0 = frequency & ( for n being Nat holds [(seq . n),(seq . (n + 1))] in fifth MS ) )
defpred S1[ set , set , set ] means ex x, y being positive Real st [$2,$3] in fifth MS;
A1:
for n being Nat
for x being Element of MS ex y being Element of MS st S1[n,x,y]
consider seq being sequence of MS such that
A2:
seq . 0 = frequency
and
A3:
for n being Nat holds S1[n,seq . n,seq . (n + 1)]
from RECDEF_1:sch 2(A1);
take
seq
; ( seq . 0 = frequency & ( for n being Nat holds [(seq . n),(seq . (n + 1))] in fifth MS ) )
hence
( seq . 0 = frequency & ( for n being Nat holds [(seq . n),(seq . (n + 1))] in fifth MS ) )
; verum