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;
( j in Seg (len m) implies ex x being Element of NAT st S1[j,x] )
assume
j in Seg (len m)
;
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 A3:
j = 2
;
ex x being Element of NAT st S1[j,x]take
ADD_MOD (
(m . 2),
(k . 2),
n)
;
( 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;
verum end; suppose A4:
j = 3
;
ex x being Element of NAT st S1[j,x]take
ADD_MOD (
(m . 3),
(k . 3),
n)
;
( 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;
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 FINSEQ_1:sch 5(A1);
take
z
; ( 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; verum