let m be non empty Element of NAT ; :: thesis: for f being PartFunc of (REAL m),(REAL 1) ex f0 being PartFunc of (REAL m),REAL st f = <>* f0
let f be PartFunc of (REAL m),(REAL 1); :: thesis: ex f0 being PartFunc of (REAL m),REAL st f = <>* f0
defpred S₁[ set ] means $1 in dom f;
deffunc H₁( set ) -> Element of REAL = (proj 1,1) . (f /. $1);
A1: for x being set st S₁[x] holds
H₁(x) in REAL ;
consider f0 being PartFunc of (REAL m),REAL such that
A2: ( ( for x being set holds
( x in dom f0 iff ( x in REAL m & S₁[x] ) ) ) & ( for x being set st x in dom f0 holds
f0 . x = H₁(x) ) ) from PARTFUN1:sch 3(A1);
take f0 ; :: thesis: f = <>* f0
for x being set st x in dom f holds
x in dom f0 by A2;
then A3: dom f c= dom f0 by TARSKI:def 3;
for x being set st x in dom f0 holds
x in dom f by A2;
then A4: dom f0 c= dom f by TARSKI:def 3;
then A5: dom f = dom f0 by A3, XBOOLE_0:def 10;
A6: rng f0 c= dom ((proj 1,1) " ) by PDIFF_1:2;
then A7: dom (((proj 1,1) " ) * f0) = dom f0 by RELAT_1:46;
for x being Element of REAL m st x in dom (<>* f0) holds
(<>* f0) . x = f . x

proof

let x be Element of REAL m; :: thesis: ( x in dom (<>* f0) implies (<>* f0) . x = f . x )
assume A8: x in dom (<>* f0) ; :: thesis: (<>* f0) . x = f . x
then (<>* f0) . x = ((proj 1,1) " ) . (f0 . x) by FUNCT_1:22;
then A9: (<>* f0) . x = ((proj 1,1) " ) . ((proj 1,1) . (f /. x)) by A8, A7, A2;
f /. x is Element of 1 -tuples_on REAL ;
then consider x0 being Element of REAL such that
A10: f /. x = <*x0*> by FINSEQ_2:117;
(proj 1,1) . (f /. x) = x0 by A10, PDIFF_1:1;
then (<>* f0) . x = f /. x by A9, A10, PDIFF_1:1;
hence (<>* f0) . x = f . x by A7, A4, A8, PARTFUN1:def 8; :: thesis: verum

end;

hence f = <>* f0 by A6, A5, RELAT_1:46, PARTFUN1:34; :: thesis: verum