:: deftheorem defines FR2FC MATRIXC1:def 8 :
for x being FinSequence of REAL holds FR2FC x = x;