let L be non empty ZeroStr ; :: thesis: for a being Element of L holds
( (a | L) . 0 = a & ( for n being Nat st n <> 0 holds
(a | L) . n = 0. L ) )
let a be Element of L; :: thesis: ( (a | L) . 0 = a & ( for n being Nat st n <> 0 holds
(a | L) . n = 0. L ) )
0 in NAT ;
then 0 in dom (0_. L) by FUNCT_2:def 1;
hence (a | L) . 0 = a by FUNCT_7:31; :: thesis: for n being Nat st n <> 0 holds
(a | L) . n = 0. L
let n be Nat; :: thesis: ( n <> 0 implies (a | L) . n = 0. L )
assume n <> 0 ; :: thesis: (a | L) . n = 0. L
hence (a | L) . n = (0_. L) . n by FUNCT_7:32
.= 0. L by ORDINAL1:def 12, FUNCOP_1:7 ;
:: thesis: verum