let z1, z2 be FinSequence of NAT ; :: thesis: ( len z1 = len m & ( for i being Nat st i in dom m holds
( ( i = 1 implies z1 . i = MUL_MOD ((m . 1),(k . 1),n) ) & ( i = 2 implies z1 . i = ADD_MOD ((m . 2),(k . 2),n) ) & ( i = 3 implies z1 . i = ADD_MOD ((m . 3),(k . 3),n) ) & ( i = 4 implies z1 . i = MUL_MOD ((m . 4),(k . 4),n) ) & ( i <> 1 & i <> 2 & i <> 3 & i <> 4 implies z1 . i = m . i ) ) ) & len z2 = len m & ( for i being Nat st i in dom m holds
( ( i = 1 implies z2 . i = MUL_MOD ((m . 1),(k . 1),n) ) & ( i = 2 implies z2 . i = ADD_MOD ((m . 2),(k . 2),n) ) & ( i = 3 implies z2 . i = ADD_MOD ((m . 3),(k . 3),n) ) & ( i = 4 implies z2 . i = MUL_MOD ((m . 4),(k . 4),n) ) & ( i <> 1 & i <> 2 & i <> 3 & i <> 4 implies z2 . i = m . i ) ) ) implies z1 = z2 )
assume that
A8: len z1 = len m and
A9: for i being Nat st i in dom m holds
( ( i = 1 implies z1 . i = MUL_MOD ((m . 1),(k . 1),n) ) & ( i = 2 implies z1 . i = ADD_MOD ((m . 2),(k . 2),n) ) & ( i = 3 implies z1 . i = ADD_MOD ((m . 3),(k . 3),n) ) & ( i = 4 implies z1 . i = MUL_MOD ((m . 4),(k . 4),n) ) & ( i <> 1 & i <> 2 & i <> 3 & i <> 4 implies z1 . i = m . i ) ) and
A10: len z2 = len m and
A11: for i being Nat st i in dom m holds
( ( i = 1 implies z2 . i = MUL_MOD ((m . 1),(k . 1),n) ) & ( i = 2 implies z2 . i = ADD_MOD ((m . 2),(k . 2),n) ) & ( i = 3 implies z2 . i = ADD_MOD ((m . 3),(k . 3),n) ) & ( i = 4 implies z2 . i = MUL_MOD ((m . 4),(k . 4),n) ) & ( i <> 1 & i <> 2 & i <> 3 & i <> 4 implies z2 . i = m . i ) ) ; :: thesis: z1 = z2
A12: dom m = Seg (len z2) by A10, FINSEQ_1:def 3
.= dom z2 by FINSEQ_1:def 3 ;

A13: now :: thesis: for j being Nat st j in dom m holds
z1 . j = z2 . j

let j be Nat; :: thesis: ( j in dom m implies z1 . j = z2 . j )
assume A14: j in dom m ; :: thesis: z1 . j = z2 . j

now :: thesis: z1 . j = z2 . j

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

suppose A15: j = 1 ; :: thesis: z1 . j = z2 . j

hence z1 . j = MUL_MOD ((m . 1),(k . 1),n) by A9, A14
.= z2 . j by A11, A14, A15 ;
:: thesis: verum

end;

suppose A16: j = 2 ; :: thesis: z1 . j = z2 . j

hence z1 . j = ADD_MOD ((m . 2),(k . 2),n) by A9, A14
.= z2 . j by A11, A14, A16 ;
:: thesis: verum

end;

suppose A17: j = 3 ; :: thesis: z1 . j = z2 . j

hence z1 . j = ADD_MOD ((m . 3),(k . 3),n) by A9, A14
.= z2 . j by A11, A14, A17 ;
:: thesis: verum

end;

suppose A18: j = 4 ; :: thesis: z1 . j = z2 . j

hence z1 . j = MUL_MOD ((m . 4),(k . 4),n) by A9, A14
.= z2 . j by A11, A14, A18 ;
:: thesis: verum

end;

suppose A19: ( j <> 1 & j <> 2 & j <> 3 & j <> 4 ) ; :: thesis: z1 . j = z2 . j

hence z1 . j = m . j by A9, A14
.= z2 . j by A11, A14, A19 ;
:: thesis: verum

end;

end;

end;

hence z1 . j = z2 . j ; :: thesis: verum

end;

dom m = Seg (len z1) by A8, FINSEQ_1:def 3
.= dom z1 by FINSEQ_1:def 3 ;
hence z1 = z2 by A12, A13, FINSEQ_1:13; :: thesis: verum