let MS be satisfying_equiv satisfying_interval satisfying_tonic satisfying_Nat satisfying_harmonic_closed MusicStruct ; for frequency being Element of MS holds 1 -harmonique (MS,frequency) = frequency
let frequency be Element of MS; 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; verum