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 (inf f) holds
(inf f) . x = inf (rng (R_EAL (f # x)))
let f be Functional_Sequence of X,REAL; :: thesis: for x being Element of X st x in dom (inf f) holds
(inf f) . x = inf (rng (R_EAL (f # x)))
let x be Element of X; :: thesis: ( x in dom (inf f) implies (inf f) . x = inf (rng (R_EAL (f # x))) )
assume x in dom (inf f) ; :: thesis: (inf f) . x = inf (rng (R_EAL (f # x)))
then (inf f) . x = inf ((R_EAL f) # x) by MESFUNC8:def 3;
hence (inf f) . x = inf (rng (R_EAL (f # x))) by Th1; :: thesis: verum