let X, Y, D be set ; :: thesis: for F being Functional_Sequence of X,Y st F is with_the_same_dom holds

F || D is with_the_same_dom

let F be Functional_Sequence of X,Y; :: thesis: ( F is with_the_same_dom implies F || D is with_the_same_dom )

assume A1: F is with_the_same_dom ; :: thesis: F || D is with_the_same_dom

let n, m be Nat; :: according to MESFUNC8:def 2 :: thesis: dom ((F || D) . n) = dom ((F || D) . m)

set G = F || D;

(F || D) . m = (F . m) | D by Def1;

then A2: dom ((F || D) . m) = (dom (F . m)) /\ D by RELAT_1:61;

(F || D) . n = (F . n) | D by Def1;

then dom ((F || D) . n) = (dom (F . n)) /\ D by RELAT_1:61;

hence dom ((F || D) . n) = dom ((F || D) . m) by A1, A2; :: thesis: verum

F || D is with_the_same_dom

let F be Functional_Sequence of X,Y; :: thesis: ( F is with_the_same_dom implies F || D is with_the_same_dom )

assume A1: F is with_the_same_dom ; :: thesis: F || D is with_the_same_dom

let n, m be Nat; :: according to MESFUNC8:def 2 :: thesis: dom ((F || D) . n) = dom ((F || D) . m)

set G = F || D;

(F || D) . m = (F . m) | D by Def1;

then A2: dom ((F || D) . m) = (dom (F . m)) /\ D by RELAT_1:61;

(F || D) . n = (F . n) | D by Def1;

then dom ((F || D) . n) = (dom (F . n)) /\ D by RELAT_1:61;

hence dom ((F || D) . n) = dom ((F || D) . m) by A1, A2; :: thesis: verum