let X be non empty set ; :: thesis: for F, G being Functional_Sequence of X,ExtREAL
for D being set st F is additive & ( for n being Nat holds G . n = (F . n) | D ) holds
G is additive
let F, G be Functional_Sequence of X,ExtREAL; :: thesis: for D being set st F is additive & ( for n being Nat holds G . n = (F . n) | D ) holds
G is additive
let D be set ; :: thesis: ( F is additive & ( for n being Nat holds G . n = (F . n) | D ) implies G is additive )
assume that
A1: F is additive and
A2: for n being Nat holds G . n = (F . n) | D ; :: thesis: G is additive
let n, m be Nat; :: according to MESFUNC9:def 5 :: thesis: ( n <> m implies for x being set holds
( not x in (dom (G . n)) /\ (dom (G . m)) or (G . n) . x <> +infty or (G . m) . x <> -infty ) )
A3: G . m = (F . m) | D by A2;
then A4: dom (G . m) c= dom (F . m) by RELAT_1:60;
assume n <> m ; :: thesis: for x being set holds
( not x in (dom (G . n)) /\ (dom (G . m)) or (G . n) . x <> +infty or (G . m) . x <> -infty )
let x be set ; :: thesis: ( not x in (dom (G . n)) /\ (dom (G . m)) or (G . n) . x <> +infty or (G . m) . x <> -infty )
assume A5: x in (dom (G . n)) /\ (dom (G . m)) ; :: thesis: ( (G . n) . x <> +infty or (G . m) . x <> -infty )
then A6: x in dom (G . m) by XBOOLE_0:def 4;
A7: G . n = (F . n) | D by A2;
then dom (G . n) c= dom (F . n) by RELAT_1:60;
then (dom (G . n)) /\ (dom (G . m)) c= (dom (F . n)) /\ (dom (F . m)) by A4, XBOOLE_1:27;
then A8: ( (F . n) . x <> +infty or (F . m) . x <> -infty ) by A1, A5;
x in dom (G . n) by A5, XBOOLE_0:def 4;
hence ( (G . n) . x <> +infty or (G . m) . x <> -infty ) by A7, A3, A8, A6, FUNCT_1:47; :: thesis: verum