let MS be non empty satisfying_equiv satisfying_interval satisfying_commutativity satisfying_Nat satisfying_harmonic_closed satisfying_fifth_constructible satisfying_octave_constructible satisfying_octave_descendent_constructible MusicStruct ; :: thesis:
let fondamentale, frequency be Element of MS; :: thesis:
defpred S₁[ set , set , set ] means ex x, y being Element of MS st
( x = $2 & y = $3 & y = Fifth_reduct (MS,fondamentale,x) );
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:
reconsider y = Fifth_reduct (MS,fondamentale,x) as Element of MS ;
take y ; :: thesis:
thus 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);
reconsider seq = seq as sequence of MS ;

now :: thesis:

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

hereby :: thesis:

let n be Nat; :: thesis:
consider x, y being Element of MS such that
A4: x = seq . n and
A5: y = seq . (n + 1) and
A6: y = Fifth_reduct (MS,fondamentale,x) by A3;
reconsider m = n + 1 as non zero Nat ;
reconsider m9 = m - 1 as Nat ;
thus seq . (n + 1) = Fifth_reduct (MS,fondamentale,(seq . n)) by A4, A5, A6; :: thesis:

end;

end;

hence ex seq being sequence of MS st
( seq . 0 = frequency & ( for n being Nat holds seq . (n + 1) = Fifth_reduct (MS,fondamentale,(seq . n)) ) ) ; :: thesis: