let p1, p2 be FinSequence of REAL ; :: thesis: ( len p1 = len p & ( for k being Nat st k in dom p1 holds
( ( p . k > 0 implies p1 . k = log a,(p . k) ) & ( p . k = 0 implies p1 . k = 0 ) ) ) & len p2 = len p & ( for k being Nat st k in dom p2 holds
( ( p . k > 0 implies p2 . k = log a,(p . k) ) & ( p . k = 0 implies p2 . k = 0 ) ) ) implies p1 = p2 )
assume that
A8: ( len p1 = len p & ( for k being Nat st k in dom p1 holds
( ( p . k > 0 implies p1 . k = log a,(p . k) ) & ( p . k = 0 implies p1 . k = 0 ) ) ) ) and
A9: ( len p2 = len p & ( for k being Nat st k in dom p2 holds
( ( p . k > 0 implies p2 . k = log a,(p . k) ) & ( p . k = 0 implies p2 . k = 0 ) ) ) ) ; :: thesis: p1 = p2
A10: dom p1 = Seg (len p2) by A8, A9, FINSEQ_1:def 3
.= dom p2 by FINSEQ_1:def 3 ;
for k being Nat st k in dom p1 holds
p1 . k = p2 . k

proof

let k be Nat; :: thesis: ( k in dom p1 implies p1 . k = p2 . k )
assume A11: k in dom p1 ; :: thesis: p1 . k = p2 . k
then A12: ( k in dom p & k in dom p2 ) by A8, A9, FINSEQ_3:31;

per cases ( p . k > 0 or p . k = 0 ) by A1, A12, Def1;

suppose A13: p . k > 0 ; :: thesis: p1 . k = p2 . k

hence p1 . k = log a,(p . k) by A8, A11
.= p2 . k by A9, A12, A13 ;
:: thesis: verum

end;

suppose A14: p . k = 0 ; :: thesis: p1 . k = p2 . k

hence p1 . k = 0 by A8, A11
.= p2 . k by A9, A12, A14 ;
:: thesis: verum

end;

end;

end;

hence p1 = p2 by A10, FINSEQ_1:17; :: thesis: verum