let p, q be Element of 64 -tuples_on BOOLEAN; ( p . 1 = r . 58 & p . 2 = r . 50 & p . 3 = r . 42 & p . 4 = r . 34 & p . 5 = r . 26 & p . 6 = r . 18 & p . 7 = r . 10 & p . 8 = r . 2 & p . 9 = r . 60 & p . 10 = r . 52 & p . 11 = r . 44 & p . 12 = r . 36 & p . 13 = r . 28 & p . 14 = r . 20 & p . 15 = r . 12 & p . 16 = r . 4 & p . 17 = r . 62 & p . 18 = r . 54 & p . 19 = r . 46 & p . 20 = r . 38 & p . 21 = r . 30 & p . 22 = r . 22 & p . 23 = r . 14 & p . 24 = r . 6 & p . 25 = r . 64 & p . 26 = r . 56 & p . 27 = r . 48 & p . 28 = r . 40 & p . 29 = r . 32 & p . 30 = r . 24 & p . 31 = r . 16 & p . 32 = r . 8 & p . 33 = r . 57 & p . 34 = r . 49 & p . 35 = r . 41 & p . 36 = r . 33 & p . 37 = r . 25 & p . 38 = r . 17 & p . 39 = r . 9 & p . 40 = r . 1 & p . 41 = r . 59 & p . 42 = r . 51 & p . 43 = r . 43 & p . 44 = r . 35 & p . 45 = r . 27 & p . 46 = r . 19 & p . 47 = r . 11 & p . 48 = r . 3 & p . 49 = r . 61 & p . 50 = r . 53 & p . 51 = r . 45 & p . 52 = r . 37 & p . 53 = r . 29 & p . 54 = r . 21 & p . 55 = r . 13 & p . 56 = r . 5 & p . 57 = r . 63 & p . 58 = r . 55 & p . 59 = r . 47 & p . 60 = r . 39 & p . 61 = r . 31 & p . 62 = r . 23 & p . 63 = r . 15 & p . 64 = r . 7 & q . 1 = r . 58 & q . 2 = r . 50 & q . 3 = r . 42 & q . 4 = r . 34 & q . 5 = r . 26 & q . 6 = r . 18 & q . 7 = r . 10 & q . 8 = r . 2 & q . 9 = r . 60 & q . 10 = r . 52 & q . 11 = r . 44 & q . 12 = r . 36 & q . 13 = r . 28 & q . 14 = r . 20 & q . 15 = r . 12 & q . 16 = r . 4 & q . 17 = r . 62 & q . 18 = r . 54 & q . 19 = r . 46 & q . 20 = r . 38 & q . 21 = r . 30 & q . 22 = r . 22 & q . 23 = r . 14 & q . 24 = r . 6 & q . 25 = r . 64 & q . 26 = r . 56 & q . 27 = r . 48 & q . 28 = r . 40 & q . 29 = r . 32 & q . 30 = r . 24 & q . 31 = r . 16 & q . 32 = r . 8 & q . 33 = r . 57 & q . 34 = r . 49 & q . 35 = r . 41 & q . 36 = r . 33 & q . 37 = r . 25 & q . 38 = r . 17 & q . 39 = r . 9 & q . 40 = r . 1 & q . 41 = r . 59 & q . 42 = r . 51 & q . 43 = r . 43 & q . 44 = r . 35 & q . 45 = r . 27 & q . 46 = r . 19 & q . 47 = r . 11 & q . 48 = r . 3 & q . 49 = r . 61 & q . 50 = r . 53 & q . 51 = r . 45 & q . 52 = r . 37 & q . 53 = r . 29 & q . 54 = r . 21 & q . 55 = r . 13 & q . 56 = r . 5 & q . 57 = r . 63 & q . 58 = r . 55 & q . 59 = r . 47 & q . 60 = r . 39 & q . 61 = r . 31 & q . 62 = r . 23 & q . 63 = r . 15 & q . 64 = r . 7 implies p = q )
assume A2:
( p . 1 = r . 58 & p . 2 = r . 50 & p . 3 = r . 42 & p . 4 = r . 34 & p . 5 = r . 26 & p . 6 = r . 18 & p . 7 = r . 10 & p . 8 = r . 2 & p . 9 = r . 60 & p . 10 = r . 52 & p . 11 = r . 44 & p . 12 = r . 36 & p . 13 = r . 28 & p . 14 = r . 20 & p . 15 = r . 12 & p . 16 = r . 4 & p . 17 = r . 62 & p . 18 = r . 54 & p . 19 = r . 46 & p . 20 = r . 38 & p . 21 = r . 30 & p . 22 = r . 22 & p . 23 = r . 14 & p . 24 = r . 6 & p . 25 = r . 64 & p . 26 = r . 56 & p . 27 = r . 48 & p . 28 = r . 40 & p . 29 = r . 32 & p . 30 = r . 24 & p . 31 = r . 16 & p . 32 = r . 8 & p . 33 = r . 57 & p . 34 = r . 49 & p . 35 = r . 41 & p . 36 = r . 33 & p . 37 = r . 25 & p . 38 = r . 17 & p . 39 = r . 9 & p . 40 = r . 1 & p . 41 = r . 59 & p . 42 = r . 51 & p . 43 = r . 43 & p . 44 = r . 35 & p . 45 = r . 27 & p . 46 = r . 19 & p . 47 = r . 11 & p . 48 = r . 3 & p . 49 = r . 61 & p . 50 = r . 53 & p . 51 = r . 45 & p . 52 = r . 37 & p . 53 = r . 29 & p . 54 = r . 21 & p . 55 = r . 13 & p . 56 = r . 5 & p . 57 = r . 63 & p . 58 = r . 55 & p . 59 = r . 47 & p . 60 = r . 39 & p . 61 = r . 31 & p . 62 = r . 23 & p . 63 = r . 15 & p . 64 = r . 7 )
; ( not q . 1 = r . 58 or not q . 2 = r . 50 or not q . 3 = r . 42 or not q . 4 = r . 34 or not q . 5 = r . 26 or not q . 6 = r . 18 or not q . 7 = r . 10 or not q . 8 = r . 2 or not q . 9 = r . 60 or not q . 10 = r . 52 or not q . 11 = r . 44 or not q . 12 = r . 36 or not q . 13 = r . 28 or not q . 14 = r . 20 or not q . 15 = r . 12 or not q . 16 = r . 4 or not q . 17 = r . 62 or not q . 18 = r . 54 or not q . 19 = r . 46 or not q . 20 = r . 38 or not q . 21 = r . 30 or not q . 22 = r . 22 or not q . 23 = r . 14 or not q . 24 = r . 6 or not q . 25 = r . 64 or not q . 26 = r . 56 or not q . 27 = r . 48 or not q . 28 = r . 40 or not q . 29 = r . 32 or not q . 30 = r . 24 or not q . 31 = r . 16 or not q . 32 = r . 8 or not q . 33 = r . 57 or not q . 34 = r . 49 or not q . 35 = r . 41 or not q . 36 = r . 33 or not q . 37 = r . 25 or not q . 38 = r . 17 or not q . 39 = r . 9 or not q . 40 = r . 1 or not q . 41 = r . 59 or not q . 42 = r . 51 or not q . 43 = r . 43 or not q . 44 = r . 35 or not q . 45 = r . 27 or not q . 46 = r . 19 or not q . 47 = r . 11 or not q . 48 = r . 3 or not q . 49 = r . 61 or not q . 50 = r . 53 or not q . 51 = r . 45 or not q . 52 = r . 37 or not q . 53 = r . 29 or not q . 54 = r . 21 or not q . 55 = r . 13 or not q . 56 = r . 5 or not q . 57 = r . 63 or not q . 58 = r . 55 or not q . 59 = r . 47 or not q . 60 = r . 39 or not q . 61 = r . 31 or not q . 62 = r . 23 or not q . 63 = r . 15 or not q . 64 = r . 7 or p = q )
assume A3:
( q . 1 = r . 58 & q . 2 = r . 50 & q . 3 = r . 42 & q . 4 = r . 34 & q . 5 = r . 26 & q . 6 = r . 18 & q . 7 = r . 10 & q . 8 = r . 2 & q . 9 = r . 60 & q . 10 = r . 52 & q . 11 = r . 44 & q . 12 = r . 36 & q . 13 = r . 28 & q . 14 = r . 20 & q . 15 = r . 12 & q . 16 = r . 4 & q . 17 = r . 62 & q . 18 = r . 54 & q . 19 = r . 46 & q . 20 = r . 38 & q . 21 = r . 30 & q . 22 = r . 22 & q . 23 = r . 14 & q . 24 = r . 6 & q . 25 = r . 64 & q . 26 = r . 56 & q . 27 = r . 48 & q . 28 = r . 40 & q . 29 = r . 32 & q . 30 = r . 24 & q . 31 = r . 16 & q . 32 = r . 8 & q . 33 = r . 57 & q . 34 = r . 49 & q . 35 = r . 41 & q . 36 = r . 33 & q . 37 = r . 25 & q . 38 = r . 17 & q . 39 = r . 9 & q . 40 = r . 1 & q . 41 = r . 59 & q . 42 = r . 51 & q . 43 = r . 43 & q . 44 = r . 35 & q . 45 = r . 27 & q . 46 = r . 19 & q . 47 = r . 11 & q . 48 = r . 3 & q . 49 = r . 61 & q . 50 = r . 53 & q . 51 = r . 45 & q . 52 = r . 37 & q . 53 = r . 29 & q . 54 = r . 21 & q . 55 = r . 13 & q . 56 = r . 5 & q . 57 = r . 63 & q . 58 = r . 55 & q . 59 = r . 47 & q . 60 = r . 39 & q . 61 = r . 31 & q . 62 = r . 23 & q . 63 = r . 15 & q . 64 = r . 7 )
; p = q
p in { s where s is Element of BOOLEAN * : len s = 64 }
;
then consider t being Element of BOOLEAN * such that
A4:
( p = t & len t = 64 )
;
q in { s where s is Element of BOOLEAN * : len s = 64 }
;
then consider s being Element of BOOLEAN * such that
A5:
( q = s & len s = 64 )
;
A6:
( dom p = Seg 64 & dom q = Seg 64 )
by A4, A5, FINSEQ_1:def 3;
for i being Nat st i in dom p holds
p . i = q . i
hence
p = q
by A6; verum