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

proof

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

now :: thesis: for f, g being Function st f in rng F & g in rng F holds
dom f = dom g

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 object such that
A5: m in dom F and
A6: g = F . m by A4, FUNCT_1:def 3;
consider n being object such that
A7: n in dom F and
A8: f = F . n by A3, FUNCT_1:def 3;
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 ;
hence F is with_the_same_dom ; :: thesis: verum

end;

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

proof

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

hereby :: thesis: verum

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

end;

end;

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