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
A7: len x = len the charact of U1 and
A8: 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
A9: len y = len the charact of U1 and
A10: 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
X: dom x = Seg (len the charact of U1) by A7, FINSEQ_1:def 3;

now

let m be Nat; :: thesis: ( m in dom x implies x . m = y . m )
assume A11: m in dom x ; :: thesis: x . m = y . m
Seg (len the charact of U2) = Seg (len the charact of U1) by A1, UNIALG_2:3;
then A12: ( m in dom the charact of U1 & m in dom the charact of U2 & m in dom x & m in dom y ) by A9, A11, X, 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 UNIALG_1:5, UNIALG_1:def 5;
reconsider h2 = the charact of U2 . m as non empty homogeneous quasi_total PartFunc of (the carrier of U2 * ),the carrier of U2 by A12, UNIALG_1:5, UNIALG_1:def 5;
( x . m = [[:h1,h2:]] & y . m = [[:h1,h2:]] ) by A8, A10, A12;
hence x . m = y . m ; :: thesis: verum

end;

hence x = y by A7, A9, FINSEQ_2:10; :: thesis: verum