defpred S₁[ set , set ] means ( ( $1 = 2 implies $2 = m . 3 ) & ( $1 = 3 implies $2 = m . 2 ) & ( $1 <> 2 & $1 <> 3 implies $2 = m . $1 ) );
A1: for k being Nat st k in Seg (len m) holds
ex x being Element of NAT st S₁[k,x]

proof

let k be Nat; :: thesis: ( k in Seg (len m) implies ex x being Element of NAT st S₁[k,x] )
assume k in Seg (len m) ; :: thesis: ex x being Element of NAT st S₁[k,x]
reconsider k = k as Nat ;

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

suppose A2: k = 2 ; :: thesis: ex x being Element of NAT st S₁[k,x]

take m . 3 ; :: thesis: S₁[k,m . 3]
thus S₁[k,m . 3] by A2; :: thesis: verum

end;

suppose A3: k = 3 ; :: thesis: ex x being Element of NAT st S₁[k,x]

take m . 2 ; :: thesis: S₁[k,m . 2]
thus S₁[k,m . 2] by A3; :: thesis: verum

end;

suppose A4: ( k <> 2 & k <> 3 ) ; :: thesis: ex x being Element of NAT st S₁[k,x]

take m . k ; :: thesis: S₁[k,m . k]
thus S₁[k,m . k] by A4; :: thesis: verum

end;

end;

end;

consider z being FinSequence of NAT such that
A5: dom z = Seg (len m) and
A6: for i being Nat st i in Seg (len m) holds
S₁[i,z . i] from FINSEQ_1:sch 5(A1);
A7: for i being Nat st i in Seg (len m) holds
IFEQ (i,2,(m . 3),(IFEQ (i,3,(m . 2),(m . i)))) = z . i

proof

let i be Nat; :: thesis: ( i in Seg (len m) implies IFEQ (i,2,(m . 3),(IFEQ (i,3,(m . 2),(m . i)))) = z . i )
assume A8: i in Seg (len m) ; :: thesis: IFEQ (i,2,(m . 3),(IFEQ (i,3,(m . 2),(m . i)))) = z . i
A9: ( i = 3 implies IFEQ (i,2,(m . 3),(IFEQ (i,3,(m . 2),(m . i)))) = m . 2 )

proof

assume A10: i = 3 ; :: thesis: IFEQ (i,2,(m . 3),(IFEQ (i,3,(m . 2),(m . i)))) = m . 2
then IFEQ (i,2,(m . 3),(IFEQ (i,3,(m . 2),(m . i)))) = IFEQ (i,3,(m . 2),(m . i)) by FUNCOP_1:def 8
.= m . 2 by A10, FUNCOP_1:def 8 ;
hence IFEQ (i,2,(m . 3),(IFEQ (i,3,(m . 2),(m . i)))) = m . 2 ; :: thesis: verum

end;

A11: ( i = 2 implies IFEQ (i,2,(m . 3),(IFEQ (i,3,(m . 2),(m . i)))) = m . 3 ) by FUNCOP_1:def 8;
( i <> 2 & i <> 3 implies IFEQ (i,2,(m . 3),(IFEQ (i,3,(m . 2),(m . i)))) = m . i )

proof

assume that
A12: i <> 2 and
A13: i <> 3 ; :: thesis: IFEQ (i,2,(m . 3),(IFEQ (i,3,(m . 2),(m . i)))) = m . i
IFEQ (i,2,(m . 3),(IFEQ (i,3,(m . 2),(m . i)))) = IFEQ (i,3,(m . 2),(m . i)) by A12, FUNCOP_1:def 8
.= m . i by A13, FUNCOP_1:def 8 ;
hence IFEQ (i,2,(m . 3),(IFEQ (i,3,(m . 2),(m . i)))) = m . i ; :: thesis: verum

end;

then ( i <> 2 & i <> 3 implies IFEQ (i,2,(m . 3),(IFEQ (i,3,(m . 2),(m . i)))) = z . i ) by A6, A8;
hence IFEQ (i,2,(m . 3),(IFEQ (i,3,(m . 2),(m . i)))) = z . i by A6, A8, A11, A9; :: thesis: verum

end;

take z ; :: thesis: ( len z = len m & ( for i being Nat st i in dom m holds
z . i = IFEQ (i,2,(m . 3),(IFEQ (i,3,(m . 2),(m . i)))) ) )
Seg (len m) = dom m by FINSEQ_1:def 3;
hence ( len z = len m & ( for i being Nat st i in dom m holds
z . i = IFEQ (i,2,(m . 3),(IFEQ (i,3,(m . 2),(m . i)))) ) ) by A5, A7, FINSEQ_1:def 3; :: thesis: verum