defpred S_{1}[ 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 S_{1}[n,y]

A5: for n being Element of NAT holds S_{1}[n,g . n]
from FUNCT_2:sch 3(A1);

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

$2 . x = (Re (f # x)) . $1 ) );

A1: for n being Element of NAT ex y being Element of PFuncs (X,REAL) st S

proof

consider g being sequence of (PFuncs (X,REAL)) such that
let n be Element of NAT ; :: thesis: ex y being Element of PFuncs (X,REAL) st S_{1}[n,y]

deffunc H_{1}( Element of X) -> Element of REAL = In (((Re (f # $1)) . n),REAL);

defpred S_{2}[ 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_{2}[x] ) ) & ( for x being Element of X st x in dom g holds

g /. x = H_{1}(x) ) )
from PARTFUN2:sch 2();

take g ; :: thesis: ( g is Element of PFuncs (X,REAL) & S_{1}[n,g] )

( x in dom g iff x in dom (f . n) ) by A2;

hence ( g is Element of PFuncs (X,REAL) & S_{1}[n,g] )
by A3, PARTFUN1:45, TARSKI:2; :: thesis: verum

end;deffunc H

defpred S

consider g being PartFunc of X,REAL such that

A2: ( ( for x being Element of X holds

( x in dom g iff S

g /. x = H

take g ; :: thesis: ( g is Element of PFuncs (X,REAL) & S

A3: now :: thesis: for x being Element of X st x in dom g holds

g . x = (Re (f # x)) . n

for x being object 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 = H_{1}(x)
by A2

.= (Re (f # x)) . n ;

hence g . x = (Re (f # x)) . n by A4, PARTFUN1:def 6; :: thesis: verum

end;assume A4: x in dom g ; :: thesis: g . x = (Re (f # x)) . n

then g /. x = H

.= (Re (f # x)) . n ;

hence g . x = (Re (f # x)) . n by A4, PARTFUN1:def 6; :: thesis: verum

( x in dom g iff x in dom (f . n) ) by A2;

hence ( g is Element of PFuncs (X,REAL) & S

A5: for n being Element of NAT holds S

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;(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