let z1, z2 be AlgSequence of L; :: thesis: ( ( for i being Nat st i < m holds
z1 . i = eval p,(x |^ i) ) & ( for i being Nat st i >= m holds
z1 . i = 0. L ) & ( for i being Nat st i < m holds
z2 . i = eval p,(x |^ i) ) & ( for i being Nat st i >= m holds
z2 . i = 0. L ) implies z1 = z2 )
assume that
A9: for i being Nat st i < m holds
z1 . i = eval p,(x |^ i) and
A10: for i being Nat st i >= m holds
z1 . i = 0. L ; :: thesis: ( ex i being Nat st
( i < m & not z2 . i = eval p,(x |^ i) ) or ex i being Nat st
( i >= m & not z2 . i = 0. L ) or z1 = z2 )
assume that
A11: for i being Nat st i < m holds
z2 . i = eval p,(x |^ i) and
A12: for i being Nat st i >= m holds
z2 . i = 0. L ; :: thesis: z1 = z2

A13: 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 u9 = u as Element of NAT by FUNCT_2:def 1;

per cases ( u9 < m or m <= u9 ) ;

suppose A14: u9 < m ; :: thesis: z1 . b₁ = z2 . b₁

hence z1 . u = eval p,(x |^ u9) by A9
.= z2 . u by A11, A14 ;
:: thesis: verum

end;

suppose A15: m <= u9 ; :: thesis: z1 . b₁ = z2 . b₁

hence z1 . u = 0. L by A10
.= z2 . u by A12, A15 ;
:: thesis: verum

end;

end;

end;

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