let n be Nat; :: thesis: 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); :: thesis: 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; :: thesis: 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); :: thesis: 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; :: thesis: ( fr = fv & F = Fv implies fr (#) F = fv (#) Fv )
assume A1: ( fr = fv & F = Fv ) ; :: thesis: 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; :: thesis: verum