let L be non empty ZeroStr ; :: thesis: for a being Element of L holds (a | L) . 0 = a
let a be Element of L; :: thesis: (a | L) . 0 = a
0 in NAT ;
then 0 in dom (0_. L) by FUNCT_2:def 1;
hence a = (a | L) . 0 by FUNCT_7:31; :: thesis: verum