let X be non empty set ; :: thesis: for f being Functional_Sequence of X,REAL
for n being natural number holds
( dom ((inferior_realsequence f) . n) = dom (f . 0 ) & ( for x being Element of X st x in dom ((inferior_realsequence f) . n) holds
((inferior_realsequence f) . n) . x = (inferior_realsequence (R_EAL (f # x))) . n ) )
let f be Functional_Sequence of X,REAL ; :: thesis: for n being natural number holds
( dom ((inferior_realsequence f) . n) = dom (f . 0 ) & ( for x being Element of X st x in dom ((inferior_realsequence f) . n) holds
((inferior_realsequence f) . n) . x = (inferior_realsequence (R_EAL (f # x))) . n ) )
let n be natural number ; :: thesis: ( dom ((inferior_realsequence f) . n) = dom (f . 0 ) & ( for x being Element of X st x in dom ((inferior_realsequence f) . n) holds
((inferior_realsequence f) . n) . x = (inferior_realsequence (R_EAL (f # x))) . n ) )
set IF = inferior_realsequence f;
dom ((inferior_realsequence f) . n) = dom ((R_EAL f) . 0 ) by MESFUNC8:def 5
.= dom (R_EAL (f . 0 )) ;
hence dom ((inferior_realsequence f) . n) = dom (f . 0 ) ; :: thesis: for x being Element of X st x in dom ((inferior_realsequence f) . n) holds
((inferior_realsequence f) . n) . x = (inferior_realsequence (R_EAL (f # x))) . n
A1: n in NAT by ORDINAL1:def 13;

hereby :: thesis: verum

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

end;