let g, h be FinSequence; :: thesis: ( len g = len f & ( for i being set st i in dom g holds
g . i = (f . i) |^ a ) & len h = len f & ( for i being set st i in dom h holds
h . i = (f . i) |^ a ) implies g = h )
assume that
A2: len g = len f and
A3: for i being set st i in dom g holds
g . i = (f . i) |^ a and
A4: len h = len f and
A5: for i being set st i in dom h holds
h . i = (f . i) |^ a ; :: thesis: g = h
A6: ( dom g = Seg (len g) & dom h = Seg (len h) ) by FINSEQ_1:def 3;
for k being Nat st k in dom g holds
g . k = h . k

proof

let k be Nat; :: thesis: ( k in dom g implies g . k = h . k )
assume A7: k in dom g ; :: thesis: g . k = h . k
thus g . k = (f . k) |^ a by A3, A7
.= h . k by A2, A4, A5, A6, A7 ; :: thesis: verum

end;

hence g = h by A2, A4, A6, FINSEQ_1:13; :: thesis: verum