let L be non empty ZeroStr ; :: thesis: for z0, z1, z2 being Element of L holds <%z0,z1,z2%> . 0 = z0
let z0, z1, z2 be Element of L; :: thesis: <%z0,z1,z2%> . 0 = z0
A1: dom (0_. L) = NAT by FUNCOP_1:13;
thus <%z0,z1,z2%> . 0 = (((0_. L) +* (0,z0)) +* (1,z1)) . 0 by FUNCT_7:32
.= ((0_. L) +* (0,z0)) . 0 by FUNCT_7:32
.= z0 by A1, FUNCT_7:31 ; :: thesis: verum