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 ;

hence f = h by A5, A7, A9, FINSEQ_1:13; :: thesis: verum

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 :: thesis: for j being Nat st j in dom f9 holds

f9 . j = h9 . j

( dom f9 = Seg (len f9) & dom h9 = Seg (len h9) )
by FINSEQ_1:def 3;f9 . j = h9 . j

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;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

hence f = h by A5, A7, A9, FINSEQ_1:13; :: thesis: verum