let z1, z2 be FinSequence of NAT ; :: thesis: ( 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)))) ; :: thesis: z1 = z2
A18: dom m = Seg (len z2) by A16, FINSEQ_1:def 3
.= dom z2 by FINSEQ_1:def 3 ;

A19: now :: thesis: for j being Nat st j in dom m holds
z1 . j = z2 . j

let j be Nat; :: thesis: ( j in dom m implies z1 . j = z2 . j )
assume A20: j in dom m ; :: thesis: z1 . j = z2 . j

now :: thesis: z1 . j = z2 . j

per cases ( j = 2 or j = 3 or ( j <> 2 & j <> 3 ) ) ;

suppose j = 2 ; :: thesis: z1 . j = z2 . j

then A21: IFEQ (j,2,(m . 3),(IFEQ (j,3,(m . 2),(m . j)))) = m . 3 by FUNCOP_1:def 8;
then z2 . j = m . 3 by A17, A20;
hence z1 . j = z2 . j by A15, A20, A21; :: thesis: verum

end;

suppose A22: j = 3 ; :: thesis: z1 . j = z2 . j

A23: ( j = 3 implies IFEQ (j,2,(m . 3),(IFEQ (j,3,(m . 2),(m . j)))) = m . 2 )

proof

assume A24: j = 3 ; :: thesis: 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 ; :: thesis: verum

end;

then z2 . j = m . 2 by A17, A20, A22;
hence z1 . j = z2 . j by A15, A20, A22, A23; :: thesis: verum

end;

suppose A25: ( j <> 2 & j <> 3 ) ; :: thesis: z1 . j = z2 . j

A26: ( 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 ; :: thesis: 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 ; :: thesis: verum

end;

then z2 . j = m . j by A17, A20, A25;
hence z1 . j = z2 . j by A15, A20, A25, A26; :: thesis: verum

end;

end;

end;

hence z1 . j = z2 . j ; :: thesis: 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; :: thesis: verum