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