let n be Nat; :: thesis: for L being non empty ZeroStr
for p being sequence of L holds (p || n) . n = 0. L
let L be non empty ZeroStr ; :: thesis: for p being sequence of L holds (p || n) . n = 0. L
let p be sequence of L; :: thesis: (p || n) . n = 0. L
dom p = NAT by FUNCT_2:def 1;
hence (p || n) . n = 0. L by FUNCT_7:31, ORDINAL1:def 12; :: thesis: verum