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
now :: thesis: for r being object st r in rng ((R_EAL f) # x) holds
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;
then rng ((R_EAL f) # x) c= REAL ;
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
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;
hence f # x = (R_EAL f) # x by FUNCT_2:12; :: thesis: verum