theorem :: PRGCOR_2:5

for a, b being FinSequence of REAL
for n being Nat st len a = len b & n > len a holds
|(a,b)| = inner_prd_prg ((FS2XFS* (a,n)),(FS2XFS* (b,n)))