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

let f be Functional_Sequence of X,REAL; :: thesis: for n being Nat holds
( dom () = dom (f . 0) & ( for x being Element of X st x in dom () holds
() . x = (inferior_realsequence (R_EAL (f # x))) . n ) )

let n be Nat; :: thesis: ( dom () = dom (f . 0) & ( for x being Element of X st x in dom () holds
() . x = (inferior_realsequence (R_EAL (f # x))) . n ) )

set IF = inferior_realsequence f;
dom () = dom (() . 0) by MESFUNC8:def 5
.= dom (R_EAL (f . 0)) ;
hence dom () = dom (f . 0) ; :: thesis: for x being Element of X st x in dom () holds
() . x = (inferior_realsequence (R_EAL (f # x))) . n

hereby :: thesis: verum
let x be Element of X; :: thesis: ( x in dom () implies () . x = (inferior_realsequence (R_EAL (f # x))) . n )
assume x in dom () ; :: thesis: () . x = (inferior_realsequence (R_EAL (f # x))) . n
then A1: () . x = (inferior_realsequence (() # x)) . n by MESFUNC8:def 5
.= inf ((() # x) ^\ n) by RINFSUP2:27 ;
(R_EAL f) # x = f # x by Th1;
hence ((inferior_realsequence f) . n) . x = (inferior_realsequence (R_EAL (f # x))) . n by ; :: thesis: verum
end;