let S be non empty satisfying_Real MusicStruct ; :: thesis: ( S is satisfying_euclidean implies S is satisfying_tonic )
assume A1: S is satisfying_euclidean ; :: thesis: S is satisfying_tonic
now :: thesis: for f1, f2, f3 being Element of S st the Ratio of S . (f1,f1) = the Ratio of S . (f2,f3) holds
f2 = f3
let f1, f2, f3 be Element of S; :: thesis: ( the Ratio of S . (f1,f1) = the Ratio of S . (f2,f3) implies f2 = f3 )
assume the Ratio of S . (f1,f1) = the Ratio of S . (f2,f3) ; :: thesis: f2 = f3
then (@ f1) / (@ f1) = the Ratio of S . (f2,f3) by A1;
then (@ f1) / (@ f1) = (@ f3) / (@ f2) by A1;
hence f2 = f3 by XCMPLX_1:58, XCMPLX_1:60; :: thesis: verum
end;
hence S is satisfying_tonic ; :: thesis: verum