let X be RealNormSpace; :: thesis: for x being Point of X
for vseq being sequence of (DualSp X)
for vseq1 being sequence of (R_NormSpace_of_BoundedLinearOperators (X,RNS_Real)) st vseq = vseq1 holds
vseq # x = vseq1 # x
let x be Point of X; :: thesis: for vseq being sequence of (DualSp X)
for vseq1 being sequence of (R_NormSpace_of_BoundedLinearOperators (X,RNS_Real)) st vseq = vseq1 holds
vseq # x = vseq1 # x
let vseq be sequence of (DualSp X); :: thesis: for vseq1 being sequence of (R_NormSpace_of_BoundedLinearOperators (X,RNS_Real)) st vseq = vseq1 holds
vseq # x = vseq1 # x
let vseq1 be sequence of (R_NormSpace_of_BoundedLinearOperators (X,RNS_Real)); :: thesis: ( vseq = vseq1 implies vseq # x = vseq1 # x )
assume AS: vseq = vseq1 ; :: thesis: vseq # x = vseq1 # x
for n being Element of NAT holds (vseq # x) . n = (vseq1 # x) . n
proof
let n be Element of NAT ; :: thesis: (vseq # x) . n = (vseq1 # x) . n
(vseq # x) . n = (vseq . n) . x by Def1;
hence (vseq # x) . n = (vseq1 # x) . n by AS, LOPBAN_5:def 2; :: thesis: verum
end;
hence vseq # x = vseq1 # x ; :: thesis: verum