let f, h be Domain-Sequence; :: thesis: ( len f = len g & ( for j being Element of dom g holds f . j = the carrier of (g . j) ) & len h = len g & ( for j being Element of dom g holds h . j = the carrier of (g . j) ) implies f = h )
assume that
A5: len f = len g and
A6: for j being Element of dom g holds f . j = the carrier of (g . j) and
A7: len h = len g and
A8: for j being Element of dom g holds h . j = the carrier of (g . j) ; :: thesis: f = h
reconsider f9 = f, h9 = h as FinSequence ;

A9: now

let j be Nat; :: thesis: ( j in dom f9 implies f9 . j = h9 . j )
assume j in dom f9 ; :: thesis: f9 . j = h9 . j
then reconsider j9 = j as Element of dom g by A5, FINSEQ_3:29;
f9 . j = the carrier of (g . j9) by A6;
hence f9 . j = h9 . j by A8; :: thesis: verum

end;

( dom f9 = Seg (len f9) & dom h9 = Seg (len h9) ) by FINSEQ_1:def 3;
hence f = h by A5, A7, A9, FINSEQ_1:13; :: thesis: verum