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 ) )
A: a | L = (0_. L) +* (0,a) by RING_4:def 5;
0 in dom (0_. L) ;
hence (a | L) . 0 = a by A, 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 A, FUNCT_7:32
.= 0. L by ORDINAL1:def 12, FUNCOP_1:7 ;
:: thesis: verum