let X be non empty set ; :: thesis: for F being Functional_Sequence of X,REAL st F is with_the_same_dom holds

abs F is with_the_same_dom

let F be Functional_Sequence of X,REAL; :: thesis: ( F is with_the_same_dom implies abs F is with_the_same_dom )

assume A1: F is with_the_same_dom ; :: thesis: abs F is with_the_same_dom

for n, m being Nat holds dom ((abs F) . n) = dom ((abs F) . m)

abs F is with_the_same_dom

let F be Functional_Sequence of X,REAL; :: thesis: ( F is with_the_same_dom implies abs F is with_the_same_dom )

assume A1: F is with_the_same_dom ; :: thesis: abs F is with_the_same_dom

for n, m being Nat holds dom ((abs F) . n) = dom ((abs F) . m)

proof

hence
abs F is with_the_same_dom
by MESFUNC8:def 2; :: thesis: verum
let n, m be Nat; :: thesis: dom ((abs F) . n) = dom ((abs F) . m)

( (abs F) . n = abs (F . n) & (abs F) . m = abs (F . m) ) by SEQFUNC:def 4;

then ( dom ((abs F) . n) = dom (F . n) & dom ((abs F) . m) = dom (F . m) ) by VALUED_1:def 11;

hence dom ((abs F) . n) = dom ((abs F) . m) by A1, MESFUNC8:def 2; :: thesis: verum

end;( (abs F) . n = abs (F . n) & (abs F) . m = abs (F . m) ) by SEQFUNC:def 4;

then ( dom ((abs F) . n) = dom (F . n) & dom ((abs F) . m) = dom (F . m) ) by VALUED_1:def 11;

hence dom ((abs F) . n) = dom ((abs F) . m) by A1, MESFUNC8:def 2; :: thesis: verum