defpred S₁[ Element of NAT , Function] means ( dom $2 = dom (f . $1) & ( for x being Element of X st x in dom $2 holds
$2 . x = (Im (f # x)) . $1 ) );
A1: for n being Element of NAT ex y being Element of PFuncs (X,REAL) st S₁[n,y]

proof

let n be Element of NAT ; :: thesis:
deffunc H₁( Element of X) -> Element of REAL = In (((Im (f # $1)) . n),REAL);
defpred S₂[ set ] means $1 in dom (f . n);
consider g being PartFunc of X,REAL such that
A2: ( ( for x being Element of X holds
( x in dom g iff S₂[x] ) ) & ( for x being Element of X st x in dom g holds
g /. x = H₁(x) ) ) from PARTFUN2:sch 2();
take g ; :: thesis:

A3: now :: thesis:

let x be Element of X; :: thesis:
assume A4: x in dom g ; :: thesis:
then g /. x = H₁(x) by A2
.= (Im (f # x)) . n ;
hence g . x = (Im (f # x)) . n by A4, PARTFUN1:def 6; :: thesis:

end;

for x being object holds
( x in dom g iff x in dom (f . n) ) by A2;
hence ( g is Element of PFuncs (X,REAL) & S₁[n,g] ) by A3, PARTFUN1:45, TARSKI:2; :: thesis:

end;

consider g being sequence of (PFuncs (X,REAL)) such that
A5: for n being Element of NAT holds S₁[n,g . n] from FUNCT_2:sch 3(A1);
reconsider g = g as Functional_Sequence of X,REAL ;
take g ; :: thesis:
thus for n being Nat holds
( dom (g . n) = dom (f . n) & ( for x being Element of X st x in dom (g . n) holds
(g . n) . x = (Im (f # x)) . n ) ) :: thesis:

proof

let n be Nat; :: thesis:
n in NAT by ORDINAL1:def 12;
hence ( dom (g . n) = dom (f . n) & ( for x being Element of X st x in dom (g . n) holds
(g . n) . x = (Im (f # x)) . n ) ) by A5; :: thesis:

end;