let z1, z2 be FinSequence of NAT ; ( len z1 = len m & ( for i being Nat st i in dom m holds
z1 . i = IFEQ (i,2,(m . 3),(IFEQ (i,3,(m . 2),(m . i)))) ) & len z2 = len m & ( for i being Nat st i in dom m holds
z2 . i = IFEQ (i,2,(m . 3),(IFEQ (i,3,(m . 2),(m . i)))) ) implies z1 = z2 )
assume that
A14:
len z1 = len m
and
A15:
for i being Nat st i in dom m holds
z1 . i = IFEQ (i,2,(m . 3),(IFEQ (i,3,(m . 2),(m . i))))
and
A16:
len z2 = len m
and
A17:
for i being Nat st i in dom m holds
z2 . i = IFEQ (i,2,(m . 3),(IFEQ (i,3,(m . 2),(m . i))))
; z1 = z2
A18: dom m =
Seg (len z2)
by A16, FINSEQ_1:def 3
.=
dom z2
by FINSEQ_1:def 3
;
A19:
now for j being Nat st j in dom m holds
z1 . j = z2 . jlet j be
Nat;
( j in dom m implies z1 . j = z2 . j )assume A20:
j in dom m
;
z1 . j = z2 . jnow z1 . j = z2 . jper cases
( j = 2 or j = 3 or ( j <> 2 & j <> 3 ) )
;
suppose A22:
j = 3
;
z1 . j = z2 . jA23:
(
j = 3 implies
IFEQ (
j,2,
(m . 3),
(IFEQ (j,3,(m . 2),(m . j))))
= m . 2 )
proof
assume A24:
j = 3
;
IFEQ (j,2,(m . 3),(IFEQ (j,3,(m . 2),(m . j)))) = m . 2
then IFEQ (
j,2,
(m . 3),
(IFEQ (j,3,(m . 2),(m . j)))) =
IFEQ (
j,3,
(m . 2),
(m . j))
by FUNCOP_1:def 8
.=
m . 2
by A24, FUNCOP_1:def 8
;
hence
IFEQ (
j,2,
(m . 3),
(IFEQ (j,3,(m . 2),(m . j))))
= m . 2
;
verum
end; then
z2 . j = m . 2
by A17, A20, A22;
hence
z1 . j = z2 . j
by A15, A20, A22, A23;
verum end; suppose A25:
(
j <> 2 &
j <> 3 )
;
z1 . j = z2 . jA26:
(
j <> 2 &
j <> 3 implies
IFEQ (
j,2,
(m . 3),
(IFEQ (j,3,(m . 2),(m . j))))
= m . j )
proof
assume that A27:
j <> 2
and A28:
j <> 3
;
IFEQ (j,2,(m . 3),(IFEQ (j,3,(m . 2),(m . j)))) = m . j
IFEQ (
j,2,
(m . 3),
(IFEQ (j,3,(m . 2),(m . j)))) =
IFEQ (
j,3,
(m . 2),
(m . j))
by A27, FUNCOP_1:def 8
.=
m . j
by A28, FUNCOP_1:def 8
;
hence
IFEQ (
j,2,
(m . 3),
(IFEQ (j,3,(m . 2),(m . j))))
= m . j
;
verum
end; then
z2 . j = m . j
by A17, A20, A25;
hence
z1 . j = z2 . j
by A15, A20, A25, A26;
verum end; end; end; hence
z1 . j = z2 . j
;
verum end;
dom m =
Seg (len z1)
by A14, FINSEQ_1:def 3
.=
dom z1
by FINSEQ_1:def 3
;
hence
z1 = z2
by A18, A19, FINSEQ_1:13; verum