let X be non empty set ; :: thesis: for F, G being Functional_Sequence of X,ExtREAL
for D being set st F is with_the_same_dom & ( for n being Nat holds G . n = (F . n) | D ) holds
G is with_the_same_dom
let F, G be Functional_Sequence of X,ExtREAL; :: thesis: for D being set st F is with_the_same_dom & ( for n being Nat holds G . n = (F . n) | D ) holds
G is with_the_same_dom
let D be set ; :: thesis: ( F is with_the_same_dom & ( for n being Nat holds G . n = (F . n) | D ) implies G is with_the_same_dom )
assume that
A1: F is with_the_same_dom and
A2: for n being Nat holds G . n = (F . n) | D ; :: thesis: G is with_the_same_dom
let n, m be Nat; :: according to MESFUNC8:def 2 :: thesis: dom (G . n) = dom (G . m)
G . m = (F . m) | D by A2;
then A3: dom (G . m) = (dom (F . m)) /\ D by RELAT_1:61;
G . n = (F . n) | D by A2;
then dom (G . n) = (dom (F . n)) /\ D by RELAT_1:61;
hence dom (G . n) = dom (G . m) by A1, A3; :: thesis: verum