theorem Th23: :: VALUED_0:23

for i, j being Nat
for X being set
for s being constant sequence of X holds s . i = s . j