let L be non empty ZeroStr ; for z0, z1, z2 being Element of L holds <%z0,z1,z2%> . 1 = z1
let z0, z1, z2 be Element of L; <%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
; verum