reconsider P = (0_. L) +* (((len p) -' 1),(p . ((len p) -' 1))) as sequence of L ;
take P ; :: thesis: ( P . ((len p) -' 1) = p . ((len p) -' 1) & ( for n being Element of NAT st n <> (len p) -' 1 holds
P . n = 0. L ) )
(len p) -' 1 in NAT ;
then (len p) -' 1 in dom (0_. L) by NORMSP_1:12;
hence P . ((len p) -' 1) = p . ((len p) -' 1) by FUNCT_7:31; :: thesis: for n being Element of NAT st n <> (len p) -' 1 holds
P . n = 0. L
let n be Element of NAT ; :: thesis: ( n <> (len p) -' 1 implies P . n = 0. L )
assume n <> (len p) -' 1 ; :: thesis: P . n = 0. L
hence P . n = (0_. L) . n by FUNCT_7:32
.= 0. L by FUNCOP_1:7 ;
:: thesis: verum