let X be non empty set ; :: thesis: for f being Functional_Sequence of X,REAL

for x being Element of X holds f # x = (R_EAL f) # x

let f be Functional_Sequence of X,REAL; :: thesis: for x being Element of X holds f # x = (R_EAL f) # x

let x be Element of X; :: thesis: f # x = (R_EAL f) # x

then reconsider RFx = (R_EAL f) # x as sequence of REAL by FUNCT_2:6;

reconsider RFx = RFx as Real_Sequence ;

for x being Element of X holds f # x = (R_EAL f) # x

let f be Functional_Sequence of X,REAL; :: thesis: for x being Element of X holds f # x = (R_EAL f) # x

let x be Element of X; :: thesis: f # x = (R_EAL f) # x

now :: thesis: for r being object st r in rng ((R_EAL f) # x) holds

r in REAL

then
rng ((R_EAL f) # x) c= REAL
;r in REAL

let r be object ; :: thesis: ( r in rng ((R_EAL f) # x) implies r in REAL )

assume r in rng ((R_EAL f) # x) ; :: thesis: r in REAL

then consider n being object such that

A1: n in NAT and

A2: ((R_EAL f) # x) . n = r by FUNCT_2:11;

reconsider n = n as Element of NAT by A1;

r = ((R_EAL f) . n) . x by A2, MESFUNC5:def 13

.= (R_EAL (f . n)) . x

.= (f . n) . x ;

hence r in REAL by XREAL_0:def 1; :: thesis: verum

end;assume r in rng ((R_EAL f) # x) ; :: thesis: r in REAL

then consider n being object such that

A1: n in NAT and

A2: ((R_EAL f) # x) . n = r by FUNCT_2:11;

reconsider n = n as Element of NAT by A1;

r = ((R_EAL f) . n) . x by A2, MESFUNC5:def 13

.= (R_EAL (f . n)) . x

.= (f . n) . x ;

hence r in REAL by XREAL_0:def 1; :: thesis: verum

then reconsider RFx = (R_EAL f) # x as sequence of REAL by FUNCT_2:6;

reconsider RFx = RFx as Real_Sequence ;

now :: thesis: for n being object st n in NAT holds

RFx . n = (f # x) . n

hence
f # x = (R_EAL f) # x
by FUNCT_2:12; :: thesis: verumRFx . n = (f # x) . n

let n be object ; :: thesis: ( n in NAT implies RFx . n = (f # x) . n )

assume n in NAT ; :: thesis: RFx . n = (f # x) . n

then reconsider n1 = n as Element of NAT ;

RFx . n = ((R_EAL f) . n1) . x by MESFUNC5:def 13

.= (R_EAL (f . n1)) . x ;

hence RFx . n = (f # x) . n by SEQFUNC:def 10; :: thesis: verum

end;assume n in NAT ; :: thesis: RFx . n = (f # x) . n

then reconsider n1 = n as Element of NAT ;

RFx . n = ((R_EAL f) . n1) . x by MESFUNC5:def 13

.= (R_EAL (f . n1)) . x ;

hence RFx . n = (f # x) . n by SEQFUNC:def 10; :: thesis: verum