let Z be set ; :: thesis:
let n, i be Element of NAT ; :: thesis:
let r be Real; :: thesis:
let f be PartFunc of Z,(REAL n); :: thesis:
A1: dom (r (#) f) = dom f by VALUED_2:def 39;
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:27;
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:27;
for z being Element of Z 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 Z; :: thesis:
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)) ; :: thesis:
then A7: z in dom ((proj (i,n)) * f) by VALUED_1:def 5;
then A8: f . z = fz by A4, PARTFUN1:def 6;
(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:12 ;
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 6;
thus ((proj (i,n)) * (r (#) f)) . z = (proj (i,n)) . ((r (#) f) . z) by A5, A6, FUNCT_1:12
.= rfz . i by A10, PDIFF_1:def 1
.= (r (#) fz) . i by A1, A4, A7, A8, A10, VALUED_2:def 39
.= (r (#) ((proj (i,n)) * f)) . z by A9, RVSUM_1:44 ; :: thesis:

end;

hence (proj (i,n)) * (r (#) f) = r (#) ((proj (i,n)) * f) by A5, PARTFUN1:5; :: thesis: