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
A3: len g = len f and
A4: for i being set st i in dom g holds
g . i = (f . i) |^ a and
A5: len h = len f and
A6: for i being set st i in dom h holds
h . i = (f . i) |^ a ; :: thesis: g = h
A7: ( 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 A8: k in dom g ; :: thesis: g . k = h . k
thus g . k = (f . k) |^ a by A4, A8
.= h . k by A3, A5, A6, A7, A8 ; :: thesis: verum

end;

hence g = h by A3, A5, A7, FINSEQ_1:17; :: thesis: verum