let n be Nat; :: thesis: (Sgm0 {n}) . 0 = n
A3: rng (Sgm0 {n}) = {n} by AC113;
A4: len (Sgm0 {n}) = card {n} by Th44;
0 in dom (Sgm0 {n}) by A4, NAT_1:45;
then (Sgm0 {n}) . 0 in rng (Sgm0 {n}) by FUNCT_1:def 5;
hence (Sgm0 {n}) . 0 = n by A3, TARSKI:def 1; :: thesis: verum