let n be Nat; :: thesis: (Sgm0 {n}) . 0 = n
len (Sgm0 {n}) = card {n} by Th20;
then 0 in dom (Sgm0 {n}) by AFINSQ_1:86;
then A1: (Sgm0 {n}) . 0 in rng (Sgm0 {n}) by FUNCT_1:def 3;
rng (Sgm0 {n}) = {n} by Def4;
hence (Sgm0 {n}) . 0 = n by A1, TARSKI:def 1; :: thesis: verum