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