let MS be satisfying_fourth_constructible MusicSpace; :: thesis: ( MS = REAL_Music implies for frequency being Element of MS ex fr being positive Real st
( frequency = fr & Fourth (MS,frequency) = (4 / 3) * fr ) )
assume A1: MS = REAL_Music ; :: thesis: for frequency being Element of MS ex fr being positive Real st
( frequency = fr & Fourth (MS,frequency) = (4 / 3) * fr )
let frequency be Element of MS; :: thesis: ex fr being positive Real st
( frequency = fr & Fourth (MS,frequency) = (4 / 3) * fr )
reconsider fr = frequency as positive Real by A1, Th1;
take fr ; :: thesis: ( frequency = fr & Fourth (MS,frequency) = (4 / 3) * fr )
thus frequency = fr ; :: thesis: Fourth (MS,frequency) = (4 / 3) * fr
consider fr9, qr9 being positive Real such that
A2: fr9 = frequency and
A3: qr9 = (4 / 3) * fr9 and
A4: [fr9,qr9] in fourth MS by A1, Th78;
reconsider qr9 = qr9 as Element of MS by A1, Th1;
qr9 = Fourth (MS,frequency) by A2, A4, Def23;
hence Fourth (MS,frequency) = (4 / 3) * fr by A2, A3; :: thesis: verum