let X be non empty set ; :: thesis: for f being Functional_Sequence of X,REAL
for x being Element of X st x in dom (f . 0 ) holds
(inferior_realsequence f) # x = inferior_realsequence (R_EAL (f # x))
let f be Functional_Sequence of X,REAL ; :: thesis: for x being Element of X st x in dom (f . 0 ) holds
(inferior_realsequence f) # x = inferior_realsequence (R_EAL (f # x))
let x be Element of X; :: thesis: ( x in dom (f . 0 ) implies (inferior_realsequence f) # x = inferior_realsequence (R_EAL (f # x)) )
set F = inferior_realsequence f;
assume A1: x in dom (f . 0 ) ; :: thesis: (inferior_realsequence f) # x = inferior_realsequence (R_EAL (f # x))

now

let n be Element of NAT ; :: thesis: ((inferior_realsequence f) # x) . n = (inferior_realsequence (R_EAL (f # x))) . n
A2: dom ((inferior_realsequence f) . n) = dom (f . 0 ) by Def5a;
((inferior_realsequence f) # x) . n = ((inferior_realsequence f) . n) . x by MESFUNC5:def 13;
hence ((inferior_realsequence f) # x) . n = (inferior_realsequence (R_EAL (f # x))) . n by A1, A2, Def5a; :: thesis: verum

end;

hence (inferior_realsequence f) # x = inferior_realsequence (R_EAL (f # x)) by FUNCT_2:113; :: thesis: verum