let z1, z2 be AlgSequence of L; :: thesis: ( ( for i being Nat st i < k holds
z1 . i = (power L) . (z,((k - i) - 1)) ) & ( for i being Nat st i >= k holds
z1 . i = 0. L ) & ( for i being Nat st i < k holds
z2 . i = (power L) . (z,((k - i) - 1)) ) & ( for i being Nat st i >= k holds
z2 . i = 0. L ) implies z1 = z2 )
assume that
A8: for i being Nat st i < k holds
z1 . i = (power L) . (z,((k - i) - 1)) and
A9: for i being Nat st i >= k holds
z1 . i = 0. L ; :: thesis: ( ex i being Nat st
( i < k & not z2 . i = (power L) . (z,((k - i) - 1)) ) or ex i being Nat st
( i >= k & not z2 . i = 0. L ) or z1 = z2 )
assume that
A10: for i being Nat st i < k holds
z2 . i = (power L) . (z,((k - i) - 1)) and
A11: for i being Nat st i >= k holds
z2 . i = 0. L ; :: thesis: z1 = z2

A12: now :: thesis: for x being object st x in dom z1 holds
z1 . x = z2 . x

let x be object ; :: thesis: ( x in dom z1 implies z1 . b₁ = z2 . b₁ )
assume x in dom z1 ; :: thesis: z1 . b₁ = z2 . b₁
then reconsider x9 = x as Element of NAT ;

per cases ( x9 < k or x9 >= k ) ;

suppose A13: x9 < k ; :: thesis: z1 . b₁ = z2 . b₁

hence z1 . x = (power L) . (z,((k - x9) - 1)) by A8
.= z2 . x by A10, A13 ;
:: thesis: verum

end;

suppose A14: x9 >= k ; :: thesis: z1 . b₁ = z2 . b₁

hence z1 . x = 0. L by A9
.= z2 . x by A11, A14 ;
:: thesis: verum

end;

end;

end;

dom z1 = NAT by FUNCT_2:def 1
.= dom z2 by FUNCT_2:def 1 ;
hence z1 = z2 by A12, FUNCT_1:2; :: thesis: verum