let z1, z2 be sequence of L; :: thesis: ( ( for i being even Nat holds

( z1 . i = p . i & ( for i being odd Nat holds z1 . i = 0. L ) ) ) & ( for i being even Nat holds

( z2 . i = p . i & ( for i being odd Nat holds z2 . i = 0. L ) ) ) implies z1 = z2 )

assume A7: for i being even Nat holds

( z1 . i = p . i & ( for i being odd Nat holds z1 . i = 0. L ) ) ; :: thesis: ( ex i being even Nat st

( z2 . i = p . i implies ex i being odd Nat st not z2 . i = 0. L ) or z1 = z2 )

assume A8: for i being even Nat holds

( z2 . i = p . i & ( for i being odd Nat holds z2 . i = 0. L ) ) ; :: thesis: z1 = z2

A9: dom z1 = NAT by FUNCT_2:def 1

.= dom z2 by FUNCT_2:def 1 ;

( z1 . i = p . i & ( for i being odd Nat holds z1 . i = 0. L ) ) ) & ( for i being even Nat holds

( z2 . i = p . i & ( for i being odd Nat holds z2 . i = 0. L ) ) ) implies z1 = z2 )

assume A7: for i being even Nat holds

( z1 . i = p . i & ( for i being odd Nat holds z1 . i = 0. L ) ) ; :: thesis: ( ex i being even Nat st

( z2 . i = p . i implies ex i being odd Nat st not z2 . i = 0. L ) or z1 = z2 )

assume A8: for i being even Nat holds

( z2 . i = p . i & ( for i being odd Nat holds z2 . i = 0. L ) ) ; :: thesis: z1 = z2

A9: dom z1 = NAT by FUNCT_2:def 1

.= dom z2 by FUNCT_2:def 1 ;

now :: thesis: for x being object st x in dom z1 holds

z1 . x = z2 . x

hence
z1 = z2
by A9, FUNCT_1:2; :: thesis: verumz1 . x = z2 . x

let x be object ; :: thesis: ( x in dom z1 implies z1 . x = z2 . x )

assume x in dom z1 ; :: thesis: z1 . x = z2 . x

then reconsider m = x as Element of NAT by FUNCT_2:def 1;

hence z1 . x = z2 . x ; :: thesis: verum

end;assume x in dom z1 ; :: thesis: z1 . x = z2 . x

then reconsider m = x as Element of NAT by FUNCT_2:def 1;

hence z1 . x = z2 . x ; :: thesis: verum