let z1, z2 be FinSequence; :: thesis: ( len z1 = r & ( for i being Nat st i in dom z1 holds
z1 . i = IDEA_P ((Line (Key,i)),n) ) & len z2 = r & ( for i being Nat st i in dom z2 holds
z2 . i = IDEA_P ((Line (Key,i)),n) ) implies z1 = z2 )
assume that
A2: len z1 = r and
A3: for i being Nat st i in dom z1 holds
z1 . i = IDEA_P ((Line (Key,i)),n) and
A4: len z2 = r and
A5: for i being Nat st i in dom z2 holds
z2 . i = IDEA_P ((Line (Key,i)),n) ; :: thesis: z1 = z2

A6: now :: thesis: for j being Nat st j in Seg r holds
z1 . j = z2 . j

let j be Nat; :: thesis: ( j in Seg r implies z1 . j = z2 . j )
assume A7: j in Seg r ; :: thesis: z1 . j = z2 . j
then A8: j in dom z2 by A4, FINSEQ_1:def 3;
j in dom z1 by A2, A7, FINSEQ_1:def 3;
then z1 . j = IDEA_P ((Line (Key,j)),n) by A3
.= z2 . j by A5, A8 ;
hence z1 . j = z2 . j ; :: thesis: verum

end;

( Seg r = dom z1 & Seg r = dom z2 ) by A2, A4, FINSEQ_1:def 3;
hence z1 = z2 by A6, FINSEQ_1:13; :: thesis: verum