let MS be non empty satisfying_equiv satisfying_interval satisfying_Nat satisfying_harmonic_closed satisfying_fifth_constructible MusicStruct ; :: thesis:
let frequency be Element of MS; :: thesis:
defpred S₁[ 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 S₁[n,x,y]

proof

let n be Nat; :: thesis:
let x be Element of MS; :: thesis:
ex q being Element of MS st [x,q] in fifth MS by Def11;
hence ex y being Element of MS st S₁[n,x,y] ; :: thesis:

end;

consider seq being sequence of MS such that
A2: seq . 0 = frequency and
A3: for n being Nat holds S₁[n,seq . n,seq . (n + 1)] from RECDEF_1:sch 2(A1);
take seq ; :: thesis:

now :: thesis:

thus seq . 0 = frequency by A2; :: thesis:

hereby :: thesis:

let n be Nat; :: thesis:
S₁[n,seq . n,seq . (n + 1)] by A3;
hence [(seq . n),(seq . (n + 1))] in fifth MS ; :: thesis:

end;

end;

hence ( seq . 0 = frequency & ( for n being Nat holds [(seq . n),(seq . (n + 1))] in fifth MS ) ) ; :: thesis: