defpred S_{1}[ 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_{1}[j,x]

A7: ( dom z = Seg (len m) & ( for i being Nat st i in Seg (len m) holds

S_{1}[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

A1: for j being Nat st j in Seg (len m) holds

ex x being Element of NAT st S

proof

consider z being FinSequence of NAT such that
let j be Nat; :: thesis: ( j in Seg (len m) implies ex x being Element of NAT st S_{1}[j,x] )

assume j in Seg (len m) ; :: thesis: ex x being Element of NAT st S_{1}[j,x]

then reconsider j = j as Element of NAT ;

end;assume j in Seg (len m) ; :: thesis: ex x being Element of NAT st S

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 ) )
;

end;

suppose A2:
j = 1
; :: thesis: ex x being Element of NAT st S_{1}[j,x]

reconsider M = MUL_MOD ((m . 1),(k . 1),n) as Element of NAT by ORDINAL1:def 12;

take M ; :: thesis: S_{1}[j,M]

thus S_{1}[j,M]
by A2; :: thesis: verum

end;take M ; :: thesis: S

thus S

suppose A3:
j = 2
; :: thesis: ex x being Element of NAT st S_{1}[j,x]

take
ADD_MOD ((m . 2),(k . 2),n)
; :: thesis: ( ADD_MOD ((m . 2),(k . 2),n) is Element of NAT & S_{1}[j, ADD_MOD ((m . 2),(k . 2),n)] )

thus ( ADD_MOD ((m . 2),(k . 2),n) is Element of NAT & S_{1}[j, ADD_MOD ((m . 2),(k . 2),n)] )
by A3; :: thesis: verum

end;thus ( ADD_MOD ((m . 2),(k . 2),n) is Element of NAT & S

suppose A4:
j = 3
; :: thesis: ex x being Element of NAT st S_{1}[j,x]

take
ADD_MOD ((m . 3),(k . 3),n)
; :: thesis: ( ADD_MOD ((m . 3),(k . 3),n) is Element of NAT & S_{1}[j, ADD_MOD ((m . 3),(k . 3),n)] )

thus ( ADD_MOD ((m . 3),(k . 3),n) is Element of NAT & S_{1}[j, ADD_MOD ((m . 3),(k . 3),n)] )
by A4; :: thesis: verum

end;thus ( ADD_MOD ((m . 3),(k . 3),n) is Element of NAT & S

suppose A5:
j = 4
; :: thesis: ex x being Element of NAT st S_{1}[j,x]

reconsider M = MUL_MOD ((m . 4),(k . 4),n) as Element of NAT by ORDINAL1:def 12;

take M ; :: thesis: S_{1}[j,M]

thus S_{1}[j,M]
by A5; :: thesis: verum

end;take M ; :: thesis: S

thus S

A7: ( dom z = Seg (len m) & ( for i being Nat st i in Seg (len m) holds

S

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