let m be non zero 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₁[ object ] means $1 in dom f;
deffunc H₁( object ) -> Element of REAL = (proj (1,1)) . (f /. $1);
A1: for x being object st S₁[x] holds
H₁(x) in REAL ;
consider f0 being PartFunc of (REAL m),REAL such that
A2: ( ( for x being object holds
( x in dom f0 iff ( x in REAL m & S₁[x] ) ) ) & ( for x being object st x in dom f0 holds
f0 . x = H₁(x) ) ) from PARTFUN1:sch 3(A1);
take f0 ; :: thesis: f = <>* f0
for x being object st x in dom f holds
x in dom f0 by A2;
then A3: dom f c= dom f0 ;
for x being object st x in dom f0 holds
x in dom f by A2;
then A4: dom f0 c= dom f ;
then A5: dom f = dom f0 by A3;
A6: rng f0 c= dom ((proj (1,1)) ") by PDIFF_1:2;
then A7: dom (((proj (1,1)) ") * f0) = dom f0 by RELAT_1:27;
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:12;
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:97;
(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 6; :: thesis: verum

end;

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