let L be Ring; :: thesis: for a being Element of L holds
( (a | L) . 0 = a & ( for n being Element of NAT st n <> 0 holds
(a | L) . n = 0. L ) )
let a be Element of L; :: thesis: ( (a | L) . 0 = a & ( for n being Element of NAT st n <> 0 holds
(a | L) . n = 0. L ) )
H: a | L = (0_. L) +* (0,a) by RING_4:def 5;
0 in dom (0_. L) ;
hence (a | L) . 0 = a by H, FUNCT_7:31; :: thesis: for n being Element of NAT st n <> 0 holds
(a | L) . n = 0. L
let n be Nat; :: thesis: ( n is Element of NAT & n <> 0 implies (a | L) . n = 0. L )
now :: 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 H, FUNCT_7:32
.= 0. L by ORDINAL1:def 12, FUNCOP_1:7 ;
:: thesis: verum
end;
hence ( n is Element of NAT & n <> 0 implies (a | L) . n = 0. L ) ; :: thesis: verum