let i be Element of NAT ; :: thesis: for Z being set
for f being PartFunc of (REAL i),REAL holds <>* (f | Z) = (<>* f) | Z
let Z be set ; :: thesis: for f being PartFunc of (REAL i),REAL holds <>* (f | Z) = (<>* f) | Z
let f be PartFunc of (REAL i),REAL; :: thesis: <>* (f | Z) = (<>* f) | Z
set W = (proj (1,1)) " ;
rng (f | Z) c= dom ((proj (1,1)) ") by PDIFF_1:2;
then dom (((proj (1,1)) ") * (f | Z)) = dom (f | Z) by RELAT_1:27
.= (dom f) /\ Z by RELAT_1:61 ;
then A1: dom (((proj (1,1)) ") * (f | Z)) = (dom (<>* f)) /\ Z by Th3;

now :: thesis: for x being object st x in dom ((<>* f) | Z) holds
(<>* (f | Z)) . x = ((<>* f) | Z) . x

let x be object ; :: thesis: ( x in dom ((<>* f) | Z) implies (<>* (f | Z)) . x = ((<>* f) | Z) . x )
assume A2: x in dom ((<>* f) | Z) ; :: thesis: (<>* (f | Z)) . x = ((<>* f) | Z) . x
then x in (dom (<>* f)) /\ Z by RELAT_1:61;
then x in (dom f) /\ Z by Th3;
then A3: ( x in Z & x in dom f ) by XBOOLE_0:def 4;
dom (((proj (1,1)) ") * (f | Z)) = dom ((<>* f) | Z) by A1, RELAT_1:61;
then (<>* (f | Z)) . x = ((proj (1,1)) ") . ((f | Z) . x) by A2, FUNCT_1:12
.= ((proj (1,1)) ") . (f . x) by A3, FUNCT_1:49
.= (((proj (1,1)) ") * f) . x by A3, FUNCT_1:13 ;
hence (<>* (f | Z)) . x = ((<>* f) | Z) . x by A2, FUNCT_1:47; :: thesis: verum

end;

hence <>* (f | Z) = (<>* f) | Z by A1, FUNCT_1:2, RELAT_1:61; :: thesis: verum