let n, i be Nat; :: thesis: for f being PartFunc of REAL,(REAL n)
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 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 :: thesis: for c being object st c in dom (((proj (i,n)) * f) | A) holds
(((proj (i,n)) * f) | A) . c = ((proj (i,n)) * (f | A)) . c

let c be object ; :: 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:61;
A7: c in dom ((proj (i,n)) * f) by A6, XBOOLE_0:def 4;
then c in dom f by A2, RELAT_1:27;
then c in (dom f) /\ A by A5, XBOOLE_0:def 4;
then A8: c in dom (f | A) by RELAT_1:61;
then c in dom ((proj (i,n)) * (f | A)) by A3, RELAT_1:27;
then ((proj (i,n)) * (f | A)) . c = (proj (i,n)) . ((f | A) . c) by FUNCT_1:12
.= (proj (i,n)) . (f . c) by A8, FUNCT_1:47
.= ((proj (i,n)) * f) . c by A7, FUNCT_1:12 ;
hence (((proj (i,n)) * f) | A) . c = ((proj (i,n)) * (f | A)) . c by A5, FUNCT_1:47; :: thesis: verum

end;

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