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

now

let n be Element of NAT ; :: thesis: ((superior_realsequence f) # x) . n = (superior_realsequence (f # x)) . n
( dom ((superior_realsequence f) . n) = dom (f . 0 ) & ((superior_realsequence f) # x) . n = ((superior_realsequence f) . n) . x ) by Def6, MESFUNC5:def 13;
hence ((superior_realsequence f) # x) . n = (superior_realsequence (f # x)) . n by A1, Def6; :: thesis: verum

end;

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