let n be Element of NAT ; :: thesis: for r being Real
for f being PartFunc of REAL ,(REAL n)
for i being Element of NAT st i in Seg n holds
(proj i,n) * (r (#) f) = r (#) ((proj i,n) * f)
let r be Real; :: thesis: for f being PartFunc of REAL ,(REAL n)
for i being Element of NAT st i in Seg n holds
(proj i,n) * (r (#) f) = r (#) ((proj i,n) * f)
let f be PartFunc of REAL ,(REAL n); :: thesis: for i being Element of NAT st i in Seg n holds
(proj i,n) * (r (#) f) = r (#) ((proj i,n) * f)
let i be Element of NAT ; :: thesis: ( i in Seg n implies (proj i,n) * (r (#) f) = r (#) ((proj i,n) * f) )
assume
i in Seg n
; :: thesis: (proj i,n) * (r (#) f) = r (#) ((proj i,n) * f)
N1:
dom (r (#) f) = dom f
by Def3;
N2:
dom (proj i,n) = REAL n
by FUNCT_2:def 1;
then
rng f c= dom (proj i,n)
;
then N3:
dom ((proj i,n) * f) = dom f
by RELAT_1:46;
then N4:
dom (r (#) ((proj i,n) * f)) = dom f
by VALUED_1:def 5;
rng (r (#) f) c= dom (proj i,n)
by N2;
then N5:
dom ((proj i,n) * (r (#) f)) = dom (r (#) ((proj i,n) * f))
by N1, N4, 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 ;
:: thesis: ( z in dom (r (#) ((proj i,n) * f)) implies ((proj i,n) * (r (#) f)) . z = (r (#) ((proj i,n) * f)) . z )
assume K1:
z in dom (r (#) ((proj i,n) * f))
;
:: thesis: ((proj i,n) * (r (#) f)) . z = (r (#) ((proj i,n) * f)) . z
then K2:
z in dom ((proj i,n) * f)
by VALUED_1:def 5;
reconsider fz =
f /. z as
Element of
n -tuples_on REAL ;
reconsider rfz =
(r (#) f) /. z as
Element of
n -tuples_on REAL ;
K3:
f . z = fz
by N3, K2, PARTFUN1:def 8;
(r (#) ((proj i,n) * f)) . z =
r * (((proj i,n) * f) . z)
by K1, VALUED_1:def 5
.=
r * ((proj i,n) . fz)
by K2, K3, FUNCT_1:22
;
then K4:
(r (#) ((proj i,n) * f)) . z = r * (fz . i)
by PDIFF_1:def 1;
K5:
(r (#) f) . z = rfz
by K2, N1, N3, PARTFUN1:def 8;
thus ((proj i,n) * (r (#) f)) . z =
(proj i,n) . ((r (#) f) . z)
by K1, N5, FUNCT_1:22
.=
rfz . i
by K5, PDIFF_1:def 1
.=
(r * fz) . i
by K2, N1, N3, Def3
.=
(r (#) ((proj i,n) * f)) . z
by K4, RVSUM_1:66
;
:: thesis: verum
end;
hence
(proj i,n) * (r (#) f) = r (#) ((proj i,n) * f)
by PARTFUN1:34, N5; :: thesis: verum