let n be Nat; for F being FinSequence of (REAL-NS n)
for fr being Function of (REAL-NS n),REAL
for Fv being FinSequence of (n -VectSp_over F_Real)
for fv being Function of (n -VectSp_over F_Real),F_Real st fr = fv & F = Fv holds
fr (#) F = fv (#) Fv
let F be FinSequence of (REAL-NS n); for fr being Function of (REAL-NS n),REAL
for Fv being FinSequence of (n -VectSp_over F_Real)
for fv being Function of (n -VectSp_over F_Real),F_Real st fr = fv & F = Fv holds
fr (#) F = fv (#) Fv
let fr be Function of (REAL-NS n),REAL; for Fv being FinSequence of (n -VectSp_over F_Real)
for fv being Function of (n -VectSp_over F_Real),F_Real st fr = fv & F = Fv holds
fr (#) F = fv (#) Fv
let Fv be FinSequence of (n -VectSp_over F_Real); for fv being Function of (n -VectSp_over F_Real),F_Real st fr = fv & F = Fv holds
fr (#) F = fv (#) Fv
let fv be Function of (n -VectSp_over F_Real),F_Real; ( fr = fv & F = Fv implies fr (#) F = fv (#) Fv )
assume A1:
( fr = fv & F = Fv )
; fr (#) F = fv (#) Fv
reconsider fr1 = fr as Function of (TOP-REAL n),REAL by Th18;
reconsider F1 = F as FinSequence of (TOP-REAL n) by Th4;
fr1 (#) F1 = fr (#) F
by Th19;
hence
fr (#) F = fv (#) Fv
by A1, MATRTOP2:3; verum