let n, i be Element of NAT ; :: thesis: for f being PartFunc of REAL ,(REAL n)
for i being Element of NAT
for A being Subset of REAL holds (proj i,n) * (f | A) = ((proj i,n) * f) | A
let f be PartFunc of REAL ,(REAL n); :: thesis: for i being Element of NAT
for A being Subset of REAL holds (proj i,n) * (f | A) = ((proj i,n) * f) | A
let i be Element of NAT ; :: thesis: for A being Subset of REAL holds (proj i,n) * (f | A) = ((proj i,n) * f) | A
let A be Subset of REAL ; :: thesis: (proj i,n) * (f | A) = ((proj i,n) * f) | A
A1: dom (proj i,n) = REAL n by FUNCT_2:def 1;
then A2: rng f c= dom (proj i,n) ;
A3: rng (f | A) c= dom (proj i,n) by A1;

A4: now

let c be set ; :: thesis: ( c in dom (((proj i,n) * f) | A) implies (((proj i,n) * f) | A) . c = ((proj i,n) * (f | A)) . c )
assume A5: c in dom (((proj i,n) * f) | A) ; :: thesis: (((proj i,n) * f) | A) . c = ((proj i,n) * (f | A)) . c
then A6: c in (dom ((proj i,n) * f)) /\ A by RELAT_1:90;
then A7: c in A by XBOOLE_0:def 4;
A8: c in dom ((proj i,n) * f) by A6, XBOOLE_0:def 4;
then c in dom f by A2, RELAT_1:46;
then c in (dom f) /\ A by A7, XBOOLE_0:def 4;
then A9: c in dom (f | A) by RELAT_1:90;
then c in dom ((proj i,n) * (f | A)) by A3, RELAT_1:46;
then ((proj i,n) * (f | A)) . c = (proj i,n) . ((f | A) . c) by FUNCT_1:22
.= (proj i,n) . (f . c) by A9, FUNCT_1:70
.= ((proj i,n) * f) . c by A8, FUNCT_1:22 ;
hence (((proj i,n) * f) | A) . c = ((proj i,n) * (f | A)) . c by A5, FUNCT_1:70; :: thesis: verum

end;

dom (((proj i,n) * f) | A) = (dom ((proj i,n) * f)) /\ A by RELAT_1:90
.= (dom f) /\ A by A2, RELAT_1:46
.= dom (f | A) by RELAT_1:90
.= dom ((proj i,n) * (f | A)) by A3, RELAT_1:46 ;
hence (proj i,n) * (f | A) = ((proj i,n) * f) | A by A4, FUNCT_1:9; :: thesis: verum