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

now :: thesis: for k being Nat st k in dom f holds
f . k = g . k

let k be Nat; :: thesis: ( k in dom f implies f . k = g . k )
assume A3: k in dom f ; :: thesis: f . k = g . k
hence f . k = f /. k by PARTFUN1:def 6
.= g /. k by A2, A3
.= g . k by A1, A3, PARTFUN1:def 6 ;
:: thesis: verum

end;

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