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)

proof

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;

hence abs F is with_the_same_dom by MESFUNC8:def 2; :: thesis: verum