let P1, P2 be sequence of L; :: thesis: ( P1 . ((len p) -' 1) = p . ((len p) -' 1) & ( for n being Element of NAT st n <> (len p) -' 1 holds
P1 . n = 0. L ) & P2 . ((len p) -' 1) = p . ((len p) -' 1) & ( for n being Element of NAT st n <> (len p) -' 1 holds
P2 . n = 0. L ) implies P1 = P2 )
assume that
A1: P1 . ((len p) -' 1) = p . ((len p) -' 1) and
A2: for n being Element of NAT st n <> (len p) -' 1 holds
P1 . n = 0. L and
A3: P2 . ((len p) -' 1) = p . ((len p) -' 1) and
A4: for n being Element of NAT st n <> (len p) -' 1 holds
P2 . n = 0. L ; :: thesis: P1 = P2

now :: thesis: for i being Element of NAT holds P1 . i = P2 . i

let i be Element of NAT ; :: thesis: P1 . b₁ = P2 . b₁

per cases ( i = (len p) -' 1 or i <> (len p) -' 1 ) ;

suppose i = (len p) -' 1 ; :: thesis: P1 . b₁ = P2 . b₁

hence P1 . i = P2 . i by A1, A3; :: thesis: verum

end;

suppose A5: i <> (len p) -' 1 ; :: thesis: P1 . b₁ = P2 . b₁

hence P1 . i = 0. L by A2
.= P2 . i by A4, A5 ;
:: thesis: verum

end;

end;

end;

hence P1 = P2 by FUNCT_2:63; :: thesis: verum