set MS = REAL_Music ;
let f1, f2 be Element of REAL_Music; :: according to MUSIC_S1:def 21 :: thesis: 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; :: thesis: 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; :: thesis: verum