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
A6: len g = len f and
A7: for i being set st i in dom g holds
g . i = (f . i) |^ a and
A8: len h = len f and
A9: for i being set st i in dom h holds
h . i = (f . i) |^ a ; :: thesis: g = h
A10: dom g = Seg (len g) by FINSEQ_1:def 3;
A11: 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 A12: k in dom g ; :: thesis: g . k = h . k
thus g . k = (f . k) |^ a by A7, A12
.= h . k by A6, A8, A9, A10, A11, A12 ; :: thesis: verum

end;

hence g = h by A6, A8, A10, A11, FINSEQ_1:17; :: thesis: verum