let h1, h2 be Element of S; :: thesis: ( [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]) ; :: thesis: h1 = h2
reconsider x = 1, y = n as Element of S by Th20;

now :: thesis: ( 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; :: thesis: 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; :: thesis: verum

end;

then frequency,h1 equiv frequency,h2 by Def08a;
hence h1 = h2 by Th24; :: thesis: verum