let V be RealLinearSpace; :: thesis: 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
let Fr be FinSequence of V; :: thesis: 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
let fr be Function of V,REAL; :: thesis: 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
let Fv be FinSequence of (RLSp2RVSp V); :: thesis: for fv being Function of (RLSp2RVSp V),F_Real st fr = fv & Fr = Fv holds
fr (#) Fr = fv (#) Fv
let fv be Function of (RLSp2RVSp V),F_Real; :: thesis: ( fr = fv & Fr = Fv implies fr (#) Fr = fv (#) Fv )
assume A1: ( fr = fv & Fr = Fv ) ; :: thesis: fr (#) Fr = fv (#) Fv
then A2: len (fv (#) Fv) = len Fr by VECTSP_6:def 5;
for i being Nat st i in dom (fv (#) Fv) holds
(fv (#) Fv) . i = (fr . (Fr /. i)) * (Fr /. i)

proof

let i be Nat; :: thesis: ( i in dom (fv (#) Fv) implies (fv (#) Fv) . i = (fr . (Fr /. i)) * (Fr /. i) )
assume i in dom (fv (#) Fv) ; :: thesis: (fv (#) Fv) . i = (fr . (Fr /. i)) * (Fr /. i)
hence (fv (#) Fv) . i = (fv . (Fv /. i)) * (Fv /. i) by VECTSP_6:def 5
.= (fr . (Fr /. i)) * (Fr /. i) by A1 ;
:: thesis: verum

end;

hence fr (#) Fr = fv (#) Fv by A2, RLVECT_2:def 7; :: thesis: verum