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
A8: ( len f = len g & ( for j being Element of dom g holds f . j = the carrier of (g . j) ) ) and
A9: ( len h = len g & ( for j being Element of dom g holds h . j = the carrier of (g . j) ) ) ; :: thesis: f = h
reconsider f' = f, h' = h as FinSequence ;
A10: ( dom f' = Seg (len f') & dom h' = Seg (len h') ) by FINSEQ_1:def 3;

now

let j be Nat; :: thesis: ( j in dom f' implies f' . j = h' . j )
assume j in dom f' ; :: thesis: f' . j = h' . j
then reconsider j' = j as Element of dom g by A8, FINSEQ_3:31;
f' . j = the carrier of (g . j') by A8;
hence f' . j = h' . j by A9; :: thesis: verum

end;

hence f = h by A8, A9, A10, FINSEQ_1:17; :: thesis: verum