let x, y be PFuncFinSequence of [: the carrier of U1, the carrier of U2:]; :: thesis: ( len x = len the charact of U1 & ( for n being Nat st n in dom x holds
for h1 being non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1
for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . n & h2 = the charact of U2 . n holds
x . n = [[:h1,h2:]] ) & len y = len the charact of U1 & ( for n being Nat st n in dom y holds
for h1 being non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1
for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . n & h2 = the charact of U2 . n holds
y . n = [[:h1,h2:]] ) implies x = y )
assume that
A8: len x = len the charact of U1 and
A9: for n being Nat st n in dom x holds
for h1 being non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1
for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . n & h2 = the charact of U2 . n holds
x . n = [[:h1,h2:]] and
A10: len y = len the charact of U1 and
A11: for n being Nat st n in dom y holds
for h1 being non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1
for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . n & h2 = the charact of U2 . n holds
y . n = [[:h1,h2:]] ; :: thesis: x = y
A12: dom x = Seg (len the charact of U1) by A8, FINSEQ_1:def 3;

now :: thesis: for m being Nat st m in dom x holds
x . m = y . m

let m be Nat; :: thesis: ( m in dom x implies x . m = y . m )
assume A13: m in dom x ; :: thesis: x . m = y . m
then m in dom the charact of U1 by A12, FINSEQ_1:def 3;
then reconsider h1 = the charact of U1 . m as non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1 by MARGREL1:def 24;
Seg (len the charact of U2) = Seg (len the charact of U1) by A1, UNIALG_2:1;
then m in dom the charact of U2 by A12, A13, FINSEQ_1:def 3;
then reconsider h2 = the charact of U2 . m as non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 by MARGREL1:def 24;
( m in dom y & x . m = [[:h1,h2:]] ) by A9, A10, A12, A13, FINSEQ_1:def 3;
hence x . m = y . m by A11; :: thesis: verum

end;

hence x = y by A8, A10, FINSEQ_2:9; :: thesis: verum