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

hereby :: thesis: verum

let x be Element of X; :: thesis: ( x in dom ((superior_realsequence f) . n) implies ((superior_realsequence f) . n) . x = (superior_realsequence (R_EAL (f # x))) . n )
assume x in dom ((superior_realsequence f) . n) ; :: thesis: ((superior_realsequence f) . n) . x = (superior_realsequence (R_EAL (f # x))) . n
then ((superior_realsequence f) . n) . x = (superior_realsequence ((R_EAL f) # x)) . n by MESFUNC8:def 6;
hence ((superior_realsequence f) . n) . x = (superior_realsequence (R_EAL (f # x))) . n by Th1; :: thesis: verum

end;