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;

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

hence
x = y
by A8, A10, FINSEQ_2:9; :: thesis: verumx . 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;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