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 A14: ( ( 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 ) ) ; :: 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 A15: ( ( 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 ) ) ; :: thesis: z1 = z2
A16: dom z1 = NAT by FUNCT_2:def 1
.= dom z2 by FUNCT_2:def 1 ;

now

let u be set ; :: thesis: ( u in dom z1 implies z1 . b₁ = z2 . b₁ )
assume u in dom z1 ; :: thesis: z1 . b₁ = z2 . b₁
then reconsider u' = u as Element of NAT by FUNCT_2:def 1;

per cases ( u' < len M or len M <= u' ) ;

suppose A17: u' < len M ; :: thesis: z1 . b₁ = z2 . b₁

hence z1 . u = M * (u' + 1),1 by A14
.= z2 . u by A15, A17 ;
:: thesis: verum

end;

suppose A18: len M <= u' ; :: thesis: z1 . b₁ = z2 . b₁

hence z1 . u = 0. L by A14
.= z2 . u by A15, A18 ;
:: thesis: verum

end;

end;

end;

hence z1 = z2 by A16, FUNCT_1:9; :: thesis: verum