let F be NAT -defined initial Function; :: thesis: for G being NAT -defined Function st dom F = dom G holds
G is initial
let G be NAT -defined Function; :: thesis: ( dom F = dom G implies G is initial )
assume dom F = dom G ; :: thesis: G is initial
hence for m, l being Nat st l in dom G & m < l holds
m in dom G by Def13; :: according to AFINSQ_1:def 12 :: thesis: verum