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