let n be Element of NAT ; for r being Real
for f being PartFunc of REAL ,(REAL n)
for i being Element of NAT holds (proj i,n) * (r (#) f) = r (#) ((proj i,n) * f)
let r be Real; for f being PartFunc of REAL ,(REAL n)
for i being Element of NAT holds (proj i,n) * (r (#) f) = r (#) ((proj i,n) * f)
let f be PartFunc of REAL ,(REAL n); for i being Element of NAT holds (proj i,n) * (r (#) f) = r (#) ((proj i,n) * f)
let i be Element of NAT ; (proj i,n) * (r (#) f) = r (#) ((proj i,n) * f)
A1:
dom (r (#) f) = dom f
by Def11;
A2:
dom (proj i,n) = REAL n
by FUNCT_2:def 1;
then A3:
rng (r (#) f) c= dom (proj i,n)
;
rng f c= dom (proj i,n)
by A2;
then A4:
dom ((proj i,n) * f) = dom f
by RELAT_1:46;
then
dom (r (#) ((proj i,n) * f)) = dom f
by VALUED_1:def 5;
then A5:
dom ((proj i,n) * (r (#) f)) = dom (r (#) ((proj i,n) * f))
by A1, A3, RELAT_1:46;
for z being Element of REAL st z in dom (r (#) ((proj i,n) * f)) holds
((proj i,n) * (r (#) f)) . z = (r (#) ((proj i,n) * f)) . z
proof
let z be
Element of
REAL ;
( z in dom (r (#) ((proj i,n) * f)) implies ((proj i,n) * (r (#) f)) . z = (r (#) ((proj i,n) * f)) . z )
reconsider fz =
f /. z as
Element of
n -tuples_on REAL ;
reconsider rfz =
(r (#) f) /. z as
Element of
n -tuples_on REAL ;
assume A6:
z in dom (r (#) ((proj i,n) * f))
;
((proj i,n) * (r (#) f)) . z = (r (#) ((proj i,n) * f)) . z
then A7:
z in dom ((proj i,n) * f)
by VALUED_1:def 5;
then A8:
f . z = fz
by A4, PARTFUN1:def 8;
(r (#) ((proj i,n) * f)) . z =
r * (((proj i,n) * f) . z)
by A6, VALUED_1:def 5
.=
r * ((proj i,n) . fz)
by A7, A8, FUNCT_1:22
;
then A9:
(r (#) ((proj i,n) * f)) . z = r * (fz . i)
by PDIFF_1:def 1;
A10:
(r (#) f) . z = rfz
by A1, A4, A7, PARTFUN1:def 8;
thus ((proj i,n) * (r (#) f)) . z =
(proj i,n) . ((r (#) f) . z)
by A5, A6, FUNCT_1:22
.=
rfz . i
by A10, PDIFF_1:def 1
.=
(r * fz) . i
by A1, A4, A7, Def11
.=
(r (#) ((proj i,n) * f)) . z
by A9, RVSUM_1:66
;
verum
end;
hence
(proj i,n) * (r (#) f) = r (#) ((proj i,n) * f)
by A5, PARTFUN1:34; verum