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 st i in Seg n 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 st i in Seg n holds
(proj i,n) * (f | A) = ((proj i,n) * f) | A
let i be Element of NAT ; :: thesis: for A being Subset of REAL st i in Seg n holds
(proj i,n) * (f | A) = ((proj i,n) * f) | A
let A be Subset of REAL ; :: thesis: ( i in Seg n implies (proj i,n) * (f | A) = ((proj i,n) * f) | A )
assume i in Seg n ; :: thesis: (proj i,n) * (f | A) = ((proj i,n) * f) | A
K1: dom (proj i,n) = REAL n by FUNCT_2:def 1;
then K2: rng f c= dom (proj i,n) ;
K3: rng (f | A) c= dom (proj i,n) by K1;
KK: dom (((proj i,n) * f) | A) = (dom ((proj i,n) * f)) /\ A by RELAT_1:90
.= (dom f) /\ A by K2, RELAT_1:46
.= dom (f | A) by RELAT_1:90
.= dom ((proj i,n) * (f | A)) by K3, RELAT_1:46 ;

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 K4: c in dom (((proj i,n) * f) | A) ; :: thesis: (((proj i,n) * f) | A) . c = ((proj i,n) * (f | A)) . c
then c in (dom ((proj i,n) * f)) /\ A by RELAT_1:90;
then K5: ( c in dom ((proj i,n) * f) & c in A ) by XBOOLE_0:def 4;
then c in dom f by K2, RELAT_1:46;
then c in (dom f) /\ A by K5, XBOOLE_0:def 4;
then K6: c in dom (f | A) by RELAT_1:90;
then c in dom ((proj i,n) * (f | A)) by K3, 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 K6, FUNCT_1:70
.= ((proj i,n) * f) . c by K5, FUNCT_1:22 ;
hence (((proj i,n) * f) | A) . c = ((proj i,n) * (f | A)) . c by K4, FUNCT_1:70; :: thesis: verum

end;

hence (proj i,n) * (f | A) = ((proj i,n) * f) | A by KK, FUNCT_1:9; :: thesis: verum