let x, y be FinSequence of NAT ; :: thesis: ( len x = len the charact of U1 & ( for n being Nat st n in dom x holds
for h being non empty homogeneous PartFunc of ( the carrier of U1 *), the carrier of U1 st h = the charact of U1 . n holds
x . n = arity h ) & len y = len the charact of U1 & ( for n being Nat st n in dom y holds
for h being non empty homogeneous PartFunc of ( the carrier of U1 *), the carrier of U1 st h = the charact of U1 . n holds
y . n = arity h ) implies x = y )
assume that
A5: len x = len the charact of U1 and
A6: for n being Nat st n in dom x holds
for h being non empty homogeneous PartFunc of ( the carrier of U1 *), the carrier of U1 st h = the charact of U1 . n holds
x . n = arity h and
A7: len y = len the charact of U1 and
A8: for n being Nat st n in dom y holds
for h being non empty homogeneous PartFunc of ( the carrier of U1 *), the carrier of U1 st h = the charact of U1 . n holds
y . n = arity h ; :: thesis: x = y

now

let m be Nat; :: thesis: ( 1 <= m & m <= len x implies x . m = y . m )
assume ( 1 <= m & m <= len x ) ; :: thesis: x . m = y . m
then A9: m in Seg (len x) by FINSEQ_1:3;
then m in dom the charact of U1 by A5, FINSEQ_1:def 3;
then reconsider h = the charact of U1 . m as non empty homogeneous PartFunc of ( the carrier of U1 *), the carrier of U1 by Th5;
m in dom x by A9, FINSEQ_1:def 3;
then A10: x . m = arity h by A6;
m in dom y by A5, A7, A9, FINSEQ_1:def 3;
hence x . m = y . m by A8, A10; :: thesis: verum

end;

hence x = y by A5, A7, FINSEQ_1:18; :: thesis: verum