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