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 :: thesis: for m being Nat st 1 <= m & m <= len x holds
x . m = y . m
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:1;
then m in dom the charact of U1 by ;
then reconsider h = the charact of U1 . m as non empty homogeneous PartFunc of ( the carrier of U1 *), the carrier of U1 ;
m in dom x by ;
then A10: x . m = arity h by A6;
m in dom y by ;
hence x . m = y . m by ; :: thesis: verum
end;
hence x = y by ; :: thesis: verum