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 Nat; :: thesis: dom (F . n) = dom (F . m)
F . n = <:{},X,Y:> by A1;
hence dom (F . n) = dom (F . m) by A1; :: thesis: verum

end;