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

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

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

end;

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

let x be object ; :: thesis: ( x in fifth MS implies x in fifth (MS,frequency) )
assume A11: x in fifth MS ; :: thesis: x in fifth (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;
reconsider y = 2, z = 3 as Element of MS by Th20;
reconsider y9 = y as positive Real ;
reconsider n = 2, m = 3 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);
A15: n -harmonique (MS,frequency),m -harmonique (MS,frequency) equiv n -harmonique (MS,y),m -harmonique (MS,y) by Def10;
reconsider n0 = 1, n1 = 2, n2 = 3 as Element of MS by Th20;
consider r1 being positive Real such that
A16: n0 = r1 and
A17: n -harmonique (MS,n0) = n * r1 by Def09;
consider r2 being positive Real such that
A18: n0 = r2 and
A19: m -harmonique (MS,n0) = m * r2 by Def09;
A20: n -harmonique (MS,n0),m -harmonique (MS,n0) equiv x1,x2 by A16, A17, A18, A19, A11, A14, EQREL_1:18;
n -harmonique (MS,y),m -harmonique (MS,y) equiv n -harmonique (MS,n0),m -harmonique (MS,n0) by Def10;
then n -harmonique (MS,y),m -harmonique (MS,y) equiv x1,x2 by A20, Th23;
then n -harmonique (MS,frequency),m -harmonique (MS,frequency) equiv x1,x2 by A15, Th23;
hence x in fifth (MS,frequency) by A14, EQREL_1:18; :: thesis: verum

end;

hence fifth (MS,frequency) = fifth MS by A0; :: thesis: verum