let z1, z2 be sequence of L; :: thesis: ( ( for i being even Nat holds
( z1 . i = 0. L & ( for i being odd Nat holds z1 . i = p . i ) ) ) & ( for i being even Nat holds
( z2 . i = 0. L & ( for i being odd Nat holds z2 . i = p . i ) ) ) implies z1 = z2 )
assume A18: for i being even Nat holds
( z1 . i = 0. L & ( for i being odd Nat holds z1 . i = p . i ) ) ; :: thesis: ( ex i being even Nat st
( z2 . i = 0. L implies ex i being odd Nat st not z2 . i = p . i ) or z1 = z2 )
assume A19: for i being even Nat holds
( z2 . i = 0. L & ( for i being odd Nat holds z2 . i = p . i ) ) ; :: thesis: z1 = z2
A20: 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

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;

now :: thesis: ( ( m is even & z1 . m = z2 . m ) or ( m is odd & z1 . m = z2 . m ) )

per cases ( m is even or m is odd ) ;

case A21: m is even ; :: thesis: z1 . m = z2 . m

hence z1 . m = 0. L by A18
.= z2 . m by A21, A19 ;
:: thesis: verum

end;

case A22: m is odd ; :: thesis: z1 . m = z2 . m

hence z1 . m = p . m by A18
.= z2 . m by A22, A19 ;
:: thesis: verum

end;

end;

end;

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

end;

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