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