let MS be satisfying_equiv satisfying_interval satisfying_tonic satisfying_Nat satisfying_harmonic_closed satisfying_linearite_harmonique satisfying_harmonique_stable MusicStruct ; :: thesis: for frequency being Element of MS holds octave (MS,frequency) = octave MS
let frequency be Element of MS; :: thesis: octave (MS,frequency) = octave MS

A1: now :: thesis: for x being object st x in octave (MS,frequency) holds
x in octave MS

let x be object ; :: thesis: ( x in octave (MS,frequency) implies x in octave MS )
assume A2: x in octave (MS,frequency) ; :: thesis: x in octave MS
then consider x1, x2 being object such that
A3: x1 in the carrier of MS and
A4: x2 in the carrier of MS and
A5: x = [x1,x2] by ZFMISC_1:def 2;
reconsider x1 = x1, x2 = x2 as Element of MS by A3, A4;
A6: NATPLUS c= the carrier of MS by Def12a;
( 1 in NATPLUS & 2 in NATPLUS ) by NAT_LAT:def 6;
then reconsider y1 = 1, y2 = 2 as Element of MS by A6;
set z = 1 -harmonique (MS,frequency);
set t = 2 -harmonique (MS,frequency);
reconsider n = 1, m = 2 as non zero Nat ;
consider r2 being positive Real such that
A7: y1 = r2 and
A8: m -harmonique (MS,y1) = m * r2 by Def09;
set a = n -harmonique (MS,frequency);
set b = m -harmonique (MS,frequency);
A9: y1 = n -harmonique (MS,y1) by Th40;
A10: n -harmonique (MS,frequency),m -harmonique (MS,frequency) equiv x1,x2 by A2, A5, EQREL_1:18;
y1,y2 equiv n -harmonique (MS,frequency),m -harmonique (MS,frequency) by A9, A7, A8, Def10;
then y1,y2 equiv x1,x2 by A10, Th23;
hence x in octave MS by A5, EQREL_1:18; :: thesis: verum

end;

now :: thesis: for x being object st x in octave MS holds
x in octave (MS,frequency)

let x be object ; :: thesis: ( x in octave MS implies x in octave (MS,frequency) )
assume A11: x in octave MS ; :: thesis: x in octave (MS,frequency)
then consider x1, x2 being object such that
A12: x1 in the carrier of MS and
A13: x2 in the carrier of MS and
A14: x = [x1,x2] by ZFMISC_1:def 2;
reconsider x1 = x1, x2 = x2 as Element of MS by A12, A13;
A15: NATPLUS c= the carrier of MS by Def12a;
( 1 in NATPLUS & 2 in NATPLUS ) by NAT_LAT:def 6;
then reconsider y = 1, z = 2 as Element of MS by A15;
reconsider y9 = y as positive Real ;
reconsider n = 1, m = 2 as non zero Nat ;
set a = n -harmonique (MS,frequency);
set b = m -harmonique (MS,frequency);
set c = n -harmonique (MS,y);
set d = m -harmonique (MS,y);
A16: n -harmonique (MS,frequency),m -harmonique (MS,frequency) equiv n -harmonique (MS,y),m -harmonique (MS,y) by Def10;
reconsider n1 = 1, n2 = 2 as Element of MS by Th20;
consider r1 being positive Real such that
A17: n1 = r1 and
A18: n -harmonique (MS,n1) = n * r1 by Def09;
consider r2 being positive Real such that
A19: n1 = r2 and
A20: m -harmonique (MS,n1) = m * r2 by Def09;
n1,n2 equiv x1,x2 by A11, A14, EQREL_1:18;
then n -harmonique (MS,frequency),m -harmonique (MS,frequency) equiv x1,x2 by A16, A17, A18, A19, A20, Th23;
hence x in octave (MS,frequency) by A14, EQREL_1:18; :: thesis: verum

end;

hence octave (MS,frequency) = octave MS by A1; :: thesis: verum