let f1, f2 be Element of RAT_Music; :: thesis: for n, m being non zero Nat holds n -harmonique (RAT_Music,f1),m -harmonique (RAT_Music,f1) equiv n -harmonique (RAT_Music,f2),m -harmonique (RAT_Music,f2)
let n, m be non zero Nat; :: thesis: n -harmonique (RAT_Music,f1),m -harmonique (RAT_Music,f1) equiv n -harmonique (RAT_Music,f2),m -harmonique (RAT_Music,f2)
set fn1 = n -harmonique (RAT_Music,f1);
set fm1 = m -harmonique (RAT_Music,f1);
set fn2 = n -harmonique (RAT_Music,f2);
set fm2 = m -harmonique (RAT_Music,f2);
reconsider r1 = f1, r2 = f2 as positive Rational by Th2;
consider fr1 being positive Real such that
A1: fr1 = f1 and
A2: n -harmonique (RAT_Music,f1) = n * fr1 by Def09;
consider fr2 being positive Real such that
A3: fr2 = f1 and
A4: m -harmonique (RAT_Music,f1) = m * fr2 by Def09;
consider fr3 being positive Real such that
A5: fr3 = f2 and
A6: n -harmonique (RAT_Music,f2) = n * fr3 by Def09;
consider fr4 being positive Real such that
A7: fr4 = f2 and
A8: m -harmonique (RAT_Music,f2) = m * fr4 by Def09;
( n -harmonique (RAT_Music,f1) = n * r1 & m -harmonique (RAT_Music,f1) = m * r1 & n -harmonique (RAT_Music,f2) = n * r2 & m -harmonique (RAT_Music,f2) = m * r2 ) by A1, A2, A3, A4, A5, A6, A7, A8;
hence n -harmonique (RAT_Music,f1),m -harmonique (RAT_Music,f1) equiv n -harmonique (RAT_Music,f2),m -harmonique (RAT_Music,f2) by Th18; :: thesis: verum