let z1, z2 be AlgSequence of L; :: thesis: ( ( for i being Nat st i <len M holds z1 . i = M * ((i + 1),1) ) & ( for i being Nat st i >=len M holds z1 . i =0. L ) & ( for i being Nat st i <len M holds z2 . i = M * ((i + 1),1) ) & ( for i being Nat st i >=len M holds z2 . i =0. L ) implies z1 = z2 ) assume that A9:
for i being Nat st i <len M holds z1 . i = M * ((i + 1),1)
and A10:
for i being Nat st i >=len M holds z1 . i =0. L
; :: thesis: ( ex i being Nat st ( i <len M & not z2 . i = M * ((i + 1),1) ) or ex i being Nat st ( i >=len M & not z2 . i =0. L ) or z1 = z2 ) assume that A11:
for i being Nat st i <len M holds z2 . i = M * ((i + 1),1)
and A12:
for i being Nat st i >=len M holds z2 . i =0. L
; :: thesis: z1 = z2