let h1, h2 be Element of S; ( [frequency,h1] in Class ( the Equidistance of S,[1,n]) & [frequency,h2] in Class ( the Equidistance of S,[1,n]) implies h1 = h2 )
assume that
A1:
[frequency,h1] in Class ( the Equidistance of S,[1,n])
and
A2:
[frequency,h2] in Class ( the Equidistance of S,[1,n])
; h1 = h2
reconsider x = 1, y = n as Element of S by Th20;
now ( the Ratio of S . (x,y) = the Ratio of S . (frequency,h1) & the Ratio of S . (x,y) = the Ratio of S . (frequency,h2) )
x,
y equiv frequency,
h1
by A1, EQREL_1:18;
hence
the
Ratio of
S . (
x,
y)
= the
Ratio of
S . (
frequency,
h1)
by Def08a;
the Ratio of S . (x,y) = the Ratio of S . (frequency,h2)
x,
y equiv frequency,
h2
by A2, EQREL_1:18;
hence
the
Ratio of
S . (
x,
y)
= the
Ratio of
S . (
frequency,
h2)
by Def08a;
verum end;
then
frequency,h1 equiv frequency,h2
by Def08a;
hence
h1 = h2
by Th24; verum