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

proof

defpred S₂[ set ] means $1 in dom (f . 0);
let n be Element of NAT ; :: thesis: ex y being Element of PFuncs (X,ExtREAL) st S₁[n,y]
deffunc H₁( Element of X) -> Element of ExtREAL = (inferior_realsequence (f # $1)) . n;
consider g being PartFunc of X,ExtREAL 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: ( g is Element of PFuncs (X,ExtREAL) & S₁[n,g] )

A3: now

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

end;

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

end;

consider g being Function of NAT,(PFuncs (X,ExtREAL)) such that
A5: for n being Element of NAT holds S₁[n,g . n] from FUNCT_2:sch 10(A1);
A6: for n being natural number holds
( dom (g . n) = dom (f . 0) & ( for x being Element of X st x in dom (g . n) holds
(g . n) . x = (inferior_realsequence (f # x)) . n ) )

proof

let n be natural number ; :: thesis: ( dom (g . n) = dom (f . 0) & ( for x being Element of X st x in dom (g . n) holds
(g . n) . x = (inferior_realsequence (f # x)) . n ) )
reconsider n9 = n as Element of NAT by ORDINAL1:def 12;
dom (g . n9) = dom (f . 0) by A5;
hence ( dom (g . n) = dom (f . 0) & ( for x being Element of X st x in dom (g . n) holds
(g . n) . x = (inferior_realsequence (f # x)) . n ) ) by A5; :: thesis: verum

end;

reconsider g = g as Functional_Sequence of X,ExtREAL ;

now

let k, l be natural number ; :: thesis: dom (g . k) = dom (g . l)
reconsider k9 = k, l9 = l as Element of NAT by ORDINAL1:def 12;
dom (g . k9) = dom (f . 0) by A5;
then dom (g . k) = dom (g . l9) by A5;
hence dom (g . k) = dom (g . l) ; :: thesis: verum

end;

then reconsider g = g as with_the_same_dom Functional_Sequence of X,ExtREAL by Def2;
take g ; :: thesis: for n being natural number holds
( dom (g . n) = dom (f . 0) & ( for x being Element of X st x in dom (g . n) holds
(g . n) . x = (inferior_realsequence (f # x)) . n ) )
thus for n being natural number holds
( dom (g . n) = dom (f . 0) & ( for x being Element of X st x in dom (g . n) holds
(g . n) . x = (inferior_realsequence (f # x)) . n ) ) by A6; :: thesis: verum