let X be non empty set ; :: thesis: for F being with_the_same_dom Functional_Sequence of X,ExtREAL
for x being Element of X
for n being Element of NAT st x in dom (inf (F ^\ n)) holds
(inf (F ^\ n)) . x = inf ((F # x) ^\ n)
let F be with_the_same_dom Functional_Sequence of X,ExtREAL; :: thesis: for x being Element of X
for n being Element of NAT st x in dom (inf (F ^\ n)) holds
(inf (F ^\ n)) . x = inf ((F # x) ^\ n)
let x be Element of X; :: thesis: for n being Element of NAT st x in dom (inf (F ^\ n)) holds
(inf (F ^\ n)) . x = inf ((F # x) ^\ n)
let n be Element of NAT ; :: thesis: ( x in dom (inf (F ^\ n)) implies (inf (F ^\ n)) . x = inf ((F # x) ^\ n) )

now :: thesis: for k being Element of NAT holds ((F ^\ n) # x) . k = ((F # x) ^\ n) . k

reconsider g = F as sequence of (PFuncs (X,ExtREAL)) ;
let k be Element of NAT ; :: thesis: ((F ^\ n) # x) . k = ((F # x) ^\ n) . k
((F ^\ n) # x) . k = ((F ^\ n) . k) . x by MESFUNC5:def 13;
then ((F ^\ n) # x) . k = (g . (n + k)) . x by NAT_1:def 3;
then ((F ^\ n) # x) . k = (F # x) . (n + k) by MESFUNC5:def 13;
hence ((F ^\ n) # x) . k = ((F # x) ^\ n) . k by NAT_1:def 3; :: thesis: verum

end;

then A1: (F ^\ n) # x = (F # x) ^\ n by FUNCT_2:63;
assume x in dom (inf (F ^\ n)) ; :: thesis: (inf (F ^\ n)) . x = inf ((F # x) ^\ n)
hence (inf (F ^\ n)) . x = inf ((F # x) ^\ n) by A1, MESFUNC8:def 3; :: thesis: verum