now :: thesis: ( RAT_Music is non empty satisfying_Real satisfying_equiv satisfying_interval satisfying_tonic satisfying_commutativity satisfying_Nat satisfying_harmonic_closed satisfying_linearite_harmonique satisfying_harmonique_stable satisfying_fifth_constructible MusicStruct & RAT_Music is non empty satisfying_Real satisfying_equiv satisfying_interval satisfying_tonic satisfying_commutativity satisfying_Nat satisfying_harmonic_closed satisfying_linearite_harmonique satisfying_harmonique_stable satisfying_fifth_constructible classical_fifth MusicStruct )

thus RAT_Music is non empty satisfying_Real satisfying_equiv satisfying_interval satisfying_tonic satisfying_commutativity satisfying_Nat satisfying_harmonic_closed satisfying_linearite_harmonique satisfying_harmonique_stable satisfying_fifth_constructible MusicStruct ; :: thesis: RAT_Music is non empty satisfying_Real satisfying_equiv satisfying_interval satisfying_tonic satisfying_commutativity satisfying_Nat satisfying_harmonic_closed satisfying_linearite_harmonique satisfying_harmonique_stable satisfying_fifth_constructible classical_fifth MusicStruct
for frequency being Element of RAT_Music ex fr being positive Real st
( frequency = fr & Fifth (RAT_Music,frequency) = (3 / 2) * fr )

proof

let frequency be Element of RAT_Music; :: thesis: ex fr being positive Real st
( frequency = fr & Fifth (RAT_Music,frequency) = (3 / 2) * fr )
ex fr being positive Rational st
( frequency = fr & Fifth (RAT_Music,frequency) = (3 / 2) * fr ) by Th39;
hence ex fr being positive Real st
( frequency = fr & Fifth (RAT_Music,frequency) = (3 / 2) * fr ) ; :: thesis: verum

end;

hence RAT_Music is non empty satisfying_Real satisfying_equiv satisfying_interval satisfying_tonic satisfying_commutativity satisfying_Nat satisfying_harmonic_closed satisfying_linearite_harmonique satisfying_harmonique_stable satisfying_fifth_constructible classical_fifth MusicStruct by Def12; :: thesis: verum

end;

hence RAT_Music is non empty satisfying_Real satisfying_equiv satisfying_interval satisfying_tonic satisfying_commutativity satisfying_Nat satisfying_harmonic_closed satisfying_linearite_harmonique satisfying_harmonique_stable satisfying_fifth_constructible classical_fifth MusicStruct ; :: thesis: verum