for V being RealLinearSpace
for F, G being FinSequence of the carrier of V
for f being Function of the carrier of V,REAL holds f (#) (F ^ G) = (f (#) F) ^ (f (#) G) by Lm1;