let F be Function; :: thesis: ( F is empty implies F is initial )
assume A1: F is empty ; :: thesis: F is initial
let n be Nat; :: according to AFINSQ_1:def 12 :: thesis: for n being Nat st n in dom F & n < n holds
n in dom F
thus for n being Nat st n in dom F & n < n holds
n in dom F by A1; :: thesis: verum