theorem Th13: :: SRINGS_5:16

for n being Nat
for f being b₁ -element FinSequence of [:REAL,REAL:] ex x being Element of [:(REAL n),(REAL n):] st
for i being Nat st i in Seg n holds
( (x `1) . i = (f /. i) `1 & (x `2) . i = (f /. i) `2 )