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

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

hence
x = y
by A5, A7, FINSEQ_1:14; :: thesis: verumx . 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 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 ;

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

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