let X be non empty set ; for S being SigmaField of X
for E being Element of S
for n being Nat
for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom & E c= dom (F . 0) & ( for m being Nat holds F . m is E -measurable ) holds
(F || E) . n is E -measurable
let S be SigmaField of X; for E being Element of S
for n being Nat
for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom & E c= dom (F . 0) & ( for m being Nat holds F . m is E -measurable ) holds
(F || E) . n is E -measurable
let E be Element of S; for n being Nat
for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom & E c= dom (F . 0) & ( for m being Nat holds F . m is E -measurable ) holds
(F || E) . n is E -measurable
let n be Nat; for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom & E c= dom (F . 0) & ( for m being Nat holds F . m is E -measurable ) holds
(F || E) . n is E -measurable
let F be Functional_Sequence of X,COMPLEX; ( F is with_the_same_dom & E c= dom (F . 0) & ( for m being Nat holds F . m is E -measurable ) implies (F || E) . n is E -measurable )
set G = F || E;
A1:
Re (F || E) = (Re F) || E
by Th21;
A2:
Im (F || E) = (Im F) || E
by Th22;
assume
F is with_the_same_dom
; ( not E c= dom (F . 0) or ex m being Nat st not F . m is E -measurable or (F || E) . n is E -measurable )
then A3:
Re F is with_the_same_dom
;
then A4:
Im F is with_the_same_dom
by Th25;
assume A5:
E c= dom (F . 0)
; ( ex m being Nat st not F . m is E -measurable or (F || E) . n is E -measurable )
assume A6:
for m being Nat holds F . m is E -measurable
; (F || E) . n is E -measurable
A7:
for m being Nat holds
( (Re F) . m is E -measurable & (Im F) . m is E -measurable )
E c= dom ((Im F) . 0)
by A5, MESFUN7C:def 12;
then
(Im (F || E)) . n is E -measurable
by A4, A2, A7, Th4;
then A8:
Im ((F || E) . n) is E -measurable
by MESFUN7C:24;
E c= dom ((Re F) . 0)
by A5, MESFUN7C:def 11;
then
(Re (F || E)) . n is E -measurable
by A3, A1, A7, Th4;
then
Re ((F || E) . n) is E -measurable
by MESFUN7C:24;
hence
(F || E) . n is E -measurable
by A8, MESFUN6C:def 1; verum