defpred S1[ 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 S1[j,x]
proof
let j be Nat; :: thesis: ( j in Seg (len m) implies ex x being Element of NAT st S1[j,x] )
assume j in Seg (len m) ; :: thesis: ex x being Element of NAT st S1[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 S1[j,x]
reconsider M = MUL_MOD ((m . 1),(k . 1),n) as Element of NAT by ORDINAL1:def 12;
take M ; :: thesis: S1[j,M]
thus S1[j,M] by A2; :: thesis: verum
end;
suppose A3: j = 2 ; :: thesis: ex x being Element of NAT st S1[j,x]
take ADD_MOD ((m . 2),(k . 2),n) ; :: thesis: ( ADD_MOD ((m . 2),(k . 2),n) is Element of NAT & S1[j, ADD_MOD ((m . 2),(k . 2),n)] )
thus ( ADD_MOD ((m . 2),(k . 2),n) is Element of NAT & S1[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 S1[j,x]
take ADD_MOD ((m . 3),(k . 3),n) ; :: thesis: ( ADD_MOD ((m . 3),(k . 3),n) is Element of NAT & S1[j, ADD_MOD ((m . 3),(k . 3),n)] )
thus ( ADD_MOD ((m . 3),(k . 3),n) is Element of NAT & S1[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 S1[j,x]
reconsider M = MUL_MOD ((m . 4),(k . 4),n) as Element of NAT by ORDINAL1:def 12;
take M ; :: thesis: S1[j,M]
thus S1[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 S1[j,x]
take m . j ; :: thesis: S1[j,m . j]
thus S1[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
S1[i,z . i] ) ) from 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 ; :: thesis: verum