defpred S₁[ set , set ] means ( ( $1 = 1 implies $2 = Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (MUL_MOD (ADD_MOD (MUL_MOD (Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n),(k . 6),n))) ) & ( $1 = 2 implies $2 = Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (ADD_MOD (MUL_MOD (Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n),(MUL_MOD (ADD_MOD (MUL_MOD (Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n),(k . 6),n),n))) ) & ( $1 = 3 implies $2 = Absval ((n -BinarySequence (m . 3)) 'xor' (n -BinarySequence (MUL_MOD (ADD_MOD (MUL_MOD (Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n),(k . 6),n))) ) & ( $1 = 4 implies $2 = Absval ((n -BinarySequence (m . 4)) 'xor' (n -BinarySequence (ADD_MOD (MUL_MOD (Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n),(MUL_MOD (ADD_MOD (MUL_MOD (Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n),(k . 6),n),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]

take Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (MUL_MOD (ADD_MOD (MUL_MOD (Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n),(k . 6),n))) ; :: thesis: S₁[j, Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (MUL_MOD (ADD_MOD (MUL_MOD (Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n),(k . 6),n)))]
thus S₁[j, Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (MUL_MOD (ADD_MOD (MUL_MOD (Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n),(k . 6),n)))] by A2; :: thesis: verum

end;

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

take Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (ADD_MOD (MUL_MOD (Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n),(MUL_MOD (ADD_MOD (MUL_MOD (Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n),(k . 6),n),n))) ; :: thesis: S₁[j, Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (ADD_MOD (MUL_MOD (Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n),(MUL_MOD (ADD_MOD (MUL_MOD (Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n),(k . 6),n),n)))]
thus S₁[j, Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (ADD_MOD (MUL_MOD (Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n),(MUL_MOD (ADD_MOD (MUL_MOD (Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n),(k . 6),n),n)))] by A3; :: thesis: verum

end;

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

take Absval ((n -BinarySequence (m . 3)) 'xor' (n -BinarySequence (MUL_MOD (ADD_MOD (MUL_MOD (Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n),(k . 6),n))) ; :: thesis: S₁[j, Absval ((n -BinarySequence (m . 3)) 'xor' (n -BinarySequence (MUL_MOD (ADD_MOD (MUL_MOD (Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n),(k . 6),n)))]
thus S₁[j, Absval ((n -BinarySequence (m . 3)) 'xor' (n -BinarySequence (MUL_MOD (ADD_MOD (MUL_MOD (Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n),(k . 6),n)))] by A4; :: thesis: verum

end;

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

take Absval ((n -BinarySequence (m . 4)) 'xor' (n -BinarySequence (ADD_MOD (MUL_MOD (Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n),(MUL_MOD (ADD_MOD (MUL_MOD (Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n),(k . 6),n),n))) ; :: thesis: S₁[j, Absval ((n -BinarySequence (m . 4)) 'xor' (n -BinarySequence (ADD_MOD (MUL_MOD (Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n),(MUL_MOD (ADD_MOD (MUL_MOD (Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n),(k . 6),n),n)))]
thus S₁[j, Absval ((n -BinarySequence (m . 4)) 'xor' (n -BinarySequence (ADD_MOD (MUL_MOD (Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n),(MUL_MOD (ADD_MOD (MUL_MOD (Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n),(k . 6),n),n)))] 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) and
A8: for i being Nat st i in Seg (len m) holds
S₁[i,z . i] from FINSEQ_1:sch 5(A1);
A9: Seg (len m) = dom m by FINSEQ_1:def 3;
take z ; :: thesis: ( len z = len m & ( for i being Element of NAT st i in dom m holds
( ( i = 1 implies z . i = Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (MUL_MOD (ADD_MOD (MUL_MOD (Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n),(k . 6),n))) ) & ( i = 2 implies z . i = Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (ADD_MOD (MUL_MOD (Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n),(MUL_MOD (ADD_MOD (MUL_MOD (Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n),(k . 6),n),n))) ) & ( i = 3 implies z . i = Absval ((n -BinarySequence (m . 3)) 'xor' (n -BinarySequence (MUL_MOD (ADD_MOD (MUL_MOD (Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n),(k . 6),n))) ) & ( i = 4 implies z . i = Absval ((n -BinarySequence (m . 4)) 'xor' (n -BinarySequence (ADD_MOD (MUL_MOD (Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n),(MUL_MOD (ADD_MOD (MUL_MOD (Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n),(k . 6),n),n))) ) & ( i <> 1 & i <> 2 & i <> 3 & i <> 4 implies z . i = m . i ) ) ) )
thus ( len z = len m & ( for i being Element of NAT st i in dom m holds
( ( i = 1 implies z . i = Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (MUL_MOD (ADD_MOD (MUL_MOD (Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n),(k . 6),n))) ) & ( i = 2 implies z . i = Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (ADD_MOD (MUL_MOD (Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n),(MUL_MOD (ADD_MOD (MUL_MOD (Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n),(k . 6),n),n))) ) & ( i = 3 implies z . i = Absval ((n -BinarySequence (m . 3)) 'xor' (n -BinarySequence (MUL_MOD (ADD_MOD (MUL_MOD (Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n),(k . 6),n))) ) & ( i = 4 implies z . i = Absval ((n -BinarySequence (m . 4)) 'xor' (n -BinarySequence (ADD_MOD (MUL_MOD (Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n),(MUL_MOD (ADD_MOD (MUL_MOD (Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n),(k . 6),n),n))) ) & ( i <> 1 & i <> 2 & i <> 3 & i <> 4 implies z . i = m . i ) ) ) ) by A7, A8, A9, FINSEQ_1:def 3; :: thesis: verum