let z1, z2 be FinSequence of Segm t; :: thesis: ( len z1 = t + 1 & ( for i being Nat st i in dom z1 holds
z1 . i = [\((frac ((i - 1) * a)) * t)/] ) & len z2 = t + 1 & ( for i being Nat st i in dom z2 holds
z2 . i = [\((frac ((i - 1) * a)) * t)/] ) implies z1 = z2 )
assume that
A13: len z1 = t + 1 and
A14: for i being Nat st i in dom z1 holds
z1 . i = [\((frac ((i - 1) * a)) * t)/] and
A15: len z2 = t + 1 and
A16: for i being Nat st i in dom z2 holds
z2 . i = [\((frac ((i - 1) * a)) * t)/] ; :: thesis: z1 = z2
A17: dom z1 = Seg (len z1) by FINSEQ_1:def 3
.= dom z2 by A13, A15, FINSEQ_1:def 3 ;
for x being Nat st x in dom z1 holds
z1 . x = z2 . x

proof

let x be Nat; :: thesis: ( x in dom z1 implies z1 . x = z2 . x )
assume A18: x in dom z1 ; :: thesis: z1 . x = z2 . x
then reconsider x9 = x as Element of NAT ;
thus z1 . x = [\((frac ((x9 - 1) * a)) * t)/] by A14, A18
.= z2 . x by A16, A17, A18 ; :: thesis: verum

end;

hence z1 = z2 by A17; :: thesis: verum