set MS = REAL_Music ;
let f1, f2 be Element of REAL_Music; MUSIC_S1:def 21 for n, m being non zero Nat holds n -harmonique (REAL_Music,f1),m -harmonique (REAL_Music,f1) equiv n -harmonique (REAL_Music,f2),m -harmonique (REAL_Music,f2)
let n, m be non zero Nat; n -harmonique (REAL_Music,f1),m -harmonique (REAL_Music,f1) equiv n -harmonique (REAL_Music,f2),m -harmonique (REAL_Music,f2)
reconsider r1 = f1, r2 = f2 as positive Real by Th1;
( ex fr1 being positive Real st
( fr1 = f1 & n -harmonique (REAL_Music,f1) = n * fr1 ) & ex fr2 being positive Real st
( fr2 = f1 & m -harmonique (REAL_Music,f1) = m * fr2 ) & ex fr3 being positive Real st
( fr3 = f2 & n -harmonique (REAL_Music,f2) = n * fr3 ) & ex fr4 being positive Real st
( fr4 = f2 & m -harmonique (REAL_Music,f2) = m * fr4 ) )
by Def09;
hence
n -harmonique (REAL_Music,f1),m -harmonique (REAL_Music,f1) equiv n -harmonique (REAL_Music,f2),m -harmonique (REAL_Music,f2)
by Th11; verum