defpred S1[ Element of NAT , Function] means ( dom \$2 = dom (f . \$1) & ( for x being Element of X st x in dom \$2 holds
\$2 . x = (Re (f # x)) . \$1 ) );
A1: for n being Element of NAT ex y being Element of PFuncs (X,REAL) st S1[n,y]
proof
let n be Element of NAT ; :: thesis: ex y being Element of PFuncs (X,REAL) st S1[n,y]
deffunc H1( Element of X) -> Element of REAL = In (((Re (f # \$1)) . n),REAL);
defpred S2[ 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 S2[x] ) ) & ( for x being Element of X st x in dom g holds
g /. x = H1(x) ) ) from take g ; :: thesis: ( g is Element of PFuncs (X,REAL) & S1[n,g] )
A3: now :: thesis: for x being Element of X st x in dom g holds
g . x = (Re (f # x)) . n
let x be Element of X; :: thesis: ( x in dom g implies g . x = (Re (f # x)) . n )
assume A4: x in dom g ; :: thesis: g . x = (Re (f # x)) . n
then g /. x = H1(x) by A2
.= (Re (f # x)) . n ;
hence g . x = (Re (f # x)) . n by ; :: thesis: verum
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) & S1[n,g] ) by ; :: thesis: verum
end;
consider g being sequence of (PFuncs (X,REAL)) such that
A5: for n being Element of NAT holds S1[n,g . n] from reconsider g = g as Functional_Sequence of X,REAL ;
take g ; :: thesis: 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 = (Re (f # x)) . n ) )

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 = (Re (f # x)) . n ) ) :: thesis: verum
proof
let n be Nat; :: thesis: ( dom (g . n) = dom (f . n) & ( for x being Element of X st x in dom (g . n) holds
(g . n) . x = (Re (f # x)) . n ) )

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 = (Re (f # x)) . n ) ) by A5; :: thesis: verum
end;