let x, y be PFuncFinSequence of [: the carrier of U1, the carrier of U2:]; ( 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:]]
; x = y
A12:
dom x = Seg (len the charact of U1)
by A8, FINSEQ_1:def 3;
now for m being Nat st m in dom x holds
x . m = y . mlet m be
Nat;
( m in dom x implies x . m = y . m )assume A13:
m in dom x
;
x . m = y . mthen
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;
verum end;
hence
x = y
by A8, A10, FINSEQ_2:9; verum