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

proof

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

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

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

reconsider M = MUL_MOD ((m . 1),(k . 1),n) as Element of NAT by ORDINAL1:def 12;
take M ; :: thesis: S₁[j,M]
thus S₁[j,M] by A2; :: thesis: verum

end;

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

take ADD_MOD ((m . 2),(k . 2),n) ; :: thesis: ( ADD_MOD ((m . 2),(k . 2),n) is Element of NAT & S₁[j, ADD_MOD ((m . 2),(k . 2),n)] )
thus ( ADD_MOD ((m . 2),(k . 2),n) is Element of NAT & S₁[j, ADD_MOD ((m . 2),(k . 2),n)] ) by A3; :: thesis: verum

end;

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

take ADD_MOD ((m . 3),(k . 3),n) ; :: thesis: ( ADD_MOD ((m . 3),(k . 3),n) is Element of NAT & S₁[j, ADD_MOD ((m . 3),(k . 3),n)] )
thus ( ADD_MOD ((m . 3),(k . 3),n) is Element of NAT & S₁[j, ADD_MOD ((m . 3),(k . 3),n)] ) by A4; :: thesis: verum

end;

suppose A5: j = 4 ; :: thesis: ex x being Element of NAT st S₁[j,x]

reconsider M = MUL_MOD ((m . 4),(k . 4),n) as Element of NAT by ORDINAL1:def 12;
take M ; :: thesis: S₁[j,M]
thus S₁[j,M] by A5; :: thesis: verum

end;

suppose A6: ( j <> 1 & j <> 2 & j <> 3 & j <> 4 ) ; :: thesis: ex x being Element of NAT st S₁[j,x]

take m . j ; :: thesis: S₁[j,m . j]
thus S₁[j,m . j] by A6; :: thesis: verum

end;

end;

end;

consider z being FinSequence of NAT such that
A7: ( dom z = Seg (len m) & ( for i being Nat st i in Seg (len m) holds
S₁[i,z . i] ) ) from FINSEQ_1:sch 5(A1);
take z ; :: thesis: ( len z = len m & ( for i being Nat st i in dom m holds
( ( i = 1 implies z . i = MUL_MOD ((m . 1),(k . 1),n) ) & ( i = 2 implies z . i = ADD_MOD ((m . 2),(k . 2),n) ) & ( i = 3 implies z . i = ADD_MOD ((m . 3),(k . 3),n) ) & ( i = 4 implies z . i = MUL_MOD ((m . 4),(k . 4),n) ) & ( i <> 1 & i <> 2 & i <> 3 & i <> 4 implies z . i = m . i ) ) ) )
dom m = Seg (len m) by FINSEQ_1:def 3;
hence ( len z = len m & ( for i being Nat st i in dom m holds
( ( i = 1 implies z . i = MUL_MOD ((m . 1),(k . 1),n) ) & ( i = 2 implies z . i = ADD_MOD ((m . 2),(k . 2),n) ) & ( i = 3 implies z . i = ADD_MOD ((m . 3),(k . 3),n) ) & ( i = 4 implies z . i = MUL_MOD ((m . 4),(k . 4),n) ) & ( i <> 1 & i <> 2 & i <> 3 & i <> 4 implies z . i = m . i ) ) ) ) by A7, FINSEQ_1:def 3; :: thesis: verum