let D be non empty set ; :: thesis: for f, g being FinSequence of D st len f = len g & ( for k being Nat st 1 <= k & k <= len f holds
f /. k = g /. k ) holds
f = g
let f, g be FinSequence of D; :: thesis: ( len f = len g & ( for k being Nat st 1 <= k & k <= len f holds
f /. k = g /. k ) implies f = g )
assume that
A1: len f = len g and
A2: for k being Nat st 1 <= k & k <= len f holds
f /. k = g /. k ; :: thesis: f = g

now :: thesis: for k being Nat st 1 <= k & k <= len f holds
f . k = g . k

let k be Nat; :: thesis: ( 1 <= k & k <= len f implies f . k = g . k )
assume A3: ( 1 <= k & k <= len f ) ; :: thesis: f . k = g . k
hence f . k = f /. k by FINSEQ_4:15
.= g /. k by A2, A3
.= g . k by A1, A3, FINSEQ_4:15 ;
:: thesis: verum

end;

hence f = g by A1; :: thesis: verum