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
# 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
# x = inferior_realsequence (R_EAL (f # x))

let x be Element of X; :: thesis: ( x in dom (f . 0) implies # x = inferior_realsequence (R_EAL (f # x)) )
set F = inferior_realsequence f;
assume A1: x in dom (f . 0) ; :: thesis: # x = inferior_realsequence (R_EAL (f # x))
now :: thesis: for n being Element of NAT holds () . n = (inferior_realsequence (R_EAL (f # x))) . n
let n be Element of NAT ; :: thesis: () . n = (inferior_realsequence (R_EAL (f # x))) . n
( dom () = dom (f . 0) & () . n = () . x ) by ;
hence ((inferior_realsequence f) # x) . n = (inferior_realsequence (R_EAL (f # x))) . n by ; :: thesis: verum
end;
hence (inferior_realsequence f) # x = inferior_realsequence (R_EAL (f # x)) by FUNCT_2:63; :: thesis: verum