let n be Nat; :: thesis: for L being non empty ZeroStr
for x being Element of L holds (seq (n,x)) . n = x
let L be non empty ZeroStr ; :: thesis: for x being Element of L holds (seq (n,x)) . n = x
let x be Element of L; :: thesis: (seq (n,x)) . n = x
dom (0_. L) = NAT ;
hence (seq (n,x)) . n = x by ORDINAL1:def 12, FUNCT_7:31; :: thesis: verum