deffunc H₁( Nat) -> Element of bool [:X,Y:] = <:{} ,X,Y:>;
consider F being Functional_Sequence of X,Y such that
A1: for n being Nat holds F . n = H₁(n) from SEQFUNC:sch 1();
take F ; :: thesis: F is with_the_same_dom

hereby :: according to MESFUNC8:def 2 :: thesis: verum

let n, m be natural number ; :: thesis: dom (F . n) = dom (F . m)
( F . n = <:{} ,X,Y:> & F . m = <:{} ,X,Y:> ) by A1;
hence dom (F . n) = dom (F . m) ; :: thesis: verum

end;