let MS be satisfying_equiv satisfying_interval satisfying_tonic satisfying_Nat satisfying_harmonic_closed MusicStruct ; :: thesis: for frequency being Element of MS holds 1 -harmonique (MS,frequency) = frequency
let frequency be Element of MS; :: thesis: 1 -harmonique (MS,frequency) = frequency
A1: NATPLUS c= the carrier of MS by Def12a;
1 in NATPLUS by NAT_LAT:def 6;
then reconsider x = 1 as Element of MS by A1;
[frequency,(1 -harmonique (MS,frequency))] in Class ( the Equidistance of MS,[1,1]) by Def08b;
then x,x equiv frequency,1 -harmonique (MS,frequency) by EQREL_1:18;
hence 1 -harmonique (MS,frequency) = frequency by Th29; :: thesis: verum