A1: ( ( for n, m being natural number holds dom (F . n) = dom (F . m) ) implies F is with_the_same_dom )

proof

assume A2: for n, m being natural number holds dom (F . n) = dom (F . m) ; :: thesis: F is with_the_same_dom

now

let f, g be Function; :: thesis: ( f in rng F & g in rng F implies dom f = dom g )
assume that
A3: f in rng F and
A4: g in rng F ; :: thesis: dom f = dom g
consider m being set such that
A5: m in dom F and
A6: g = F . m by A4, FUNCT_1:def 5;
consider n being set such that
A7: n in dom F and
A8: f = F . n by A3, FUNCT_1:def 5;
reconsider n = n, m = m as Nat by A7, A5;
dom (F . n) = dom (F . m) by A2;
hence dom f = dom g by A8, A6; :: thesis: verum

end;

then rng F is with_common_domain by CARD_3:def 10;
hence F is with_the_same_dom by Def1; :: thesis: verum

end;

( F is with_the_same_dom implies for n, m being natural number holds dom (F . n) = dom (F . m) )

proof

assume F is with_the_same_dom ; :: thesis: for n, m being natural number holds dom (F . n) = dom (F . m)
then A9: rng F is with_common_domain by Def1;

hereby :: thesis: verum

let n, m be natural number ; :: thesis: dom (F . n) = dom (F . m)
A10: dom F = NAT by FUNCT_2:def 1;
then m in dom F by ORDINAL1:def 13;
then A11: F . m in rng F by FUNCT_1:12;
n in dom F by A10, ORDINAL1:def 13;
then F . n in rng F by FUNCT_1:12;
hence dom (F . n) = dom (F . m) by A9, A11, CARD_3:def 10; :: thesis: verum

end;

end;

hence ( F is with_the_same_dom iff for n, m being natural number holds dom (F . n) = dom (F . m) ) by A1; :: thesis: verum