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

.= dom z2 by FUNCT_2:def 1 ;

hence z1 = z2 by A13, FUNCT_1:2; :: thesis: verum

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

A13: now :: thesis: for u being object st u in dom z1 holds

z1 . u = z2 . u

dom z1 =
NAT
by FUNCT_2:def 1
z1 . u = z2 . u

let u be object ; :: thesis: ( u in dom z1 implies z1 . b_{1} = z2 . b_{1} )

assume u in dom z1 ; :: thesis: z1 . b_{1} = z2 . b_{1}

then reconsider u9 = u as Element of NAT by FUNCT_2:def 1;

end;assume u in dom z1 ; :: thesis: z1 . b

then reconsider u9 = u as Element of NAT by FUNCT_2:def 1;

.= dom z2 by FUNCT_2:def 1 ;

hence z1 = z2 by A13, FUNCT_1:2; :: thesis: verum