for V being RealLinearSpace
for Fr being FinSequence of V
for fr being Function of V,REAL
for Fv being FinSequence of (RLSp2RVSp V)
for fv being Function of (RLSp2RVSp V),F_Real st fr = fv & Fr = Fv holds
fr (#) Fr = fv (#) Fv