theorem :: AFINSQ_1:67

for F being NAT -defined initial Function
for G being NAT -defined Function st dom F = dom G holds
G is initial by Def12;