let L be non empty ZeroStr ; :: thesis: for z0, z1 being Element of L holds
( <%z0,z1%> . 0 = z0 & <%z0,z1%> . 1 = z1 & ( for n being Nat st n >= 2 holds
<%z0,z1%> . n = 0. L ) )
let z0, z1 be Element of L; :: thesis: ( <%z0,z1%> . 0 = z0 & <%z0,z1%> . 1 = z1 & ( for n being Nat st n >= 2 holds
<%z0,z1%> . n = 0. L ) )
0 in NAT ;
then A1: 0 in dom (0_. L) by FUNCT_2:def 1;
thus <%z0,z1%> . 0 = ((0_. L) +* (0,z0)) . 0 by FUNCT_7:32
.= z0 by A1, FUNCT_7:31 ; :: thesis: ( <%z0,z1%> . 1 = z1 & ( for n being Nat st n >= 2 holds
<%z0,z1%> . n = 0. L ) )
1 in NAT ;
then 1 in dom ((0_. L) +* (0,z0)) by FUNCT_2:def 1;
hence <%z0,z1%> . 1 = z1 by FUNCT_7:31; :: thesis: for n being Nat st n >= 2 holds
<%z0,z1%> . n = 0. L
let n be Nat; :: thesis: ( n >= 2 implies <%z0,z1%> . n = 0. L )
A2: n in NAT by ORDINAL1:def 12;
assume A3: n >= 2 ; :: thesis: <%z0,z1%> . n = 0. L
then n >= 1 + 1 ;
then n > 0 + 1 by NAT_1:13;
hence <%z0,z1%> . n = ((0_. L) +* (0,z0)) . n by FUNCT_7:32
.= (0_. L) . n by A3, FUNCT_7:32
.= 0. L by A2, FUNCOP_1:7 ;
:: thesis: verum