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
A7: len p1 = len p and
A8: 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 and
A10: 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
A11: 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 A12: k in dom p1 ; :: thesis: p1 . k = p2 . k
then A13: k in dom p by A7, FINSEQ_3:29;
A14: k in dom p2 by A7, A9, A12, FINSEQ_3:29;
per cases ( p . k > 0 or p . k = 0 ) by A1, A13;
suppose A15: p . k > 0 ; :: thesis: p1 . k = p2 . k
hence p1 . k = log (a,(p . k)) by A8, A12
.= p2 . k by A10, A14, A15 ;
:: thesis: verum
end;
suppose A16: p . k = 0 ; :: thesis: p1 . k = p2 . k
hence p1 . k = 0 by A8, A12
.= p2 . k by A10, A14, A16 ;
:: thesis: verum
end;
end;
end;
dom p1 = Seg (len p2) by A7, A9, FINSEQ_1:def 3
.= dom p2 by FINSEQ_1:def 3 ;
hence p1 = p2 by A11, FINSEQ_1:13; :: thesis: verum