let p, q be Element of 48 -tuples_on BOOLEAN; ( p . 1 = r . 14 & p . 2 = r . 17 & p . 3 = r . 11 & p . 4 = r . 24 & p . 5 = r . 1 & p . 6 = r . 5 & p . 7 = r . 3 & p . 8 = r . 28 & p . 9 = r . 15 & p . 10 = r . 6 & p . 11 = r . 21 & p . 12 = r . 10 & p . 13 = r . 23 & p . 14 = r . 19 & p . 15 = r . 12 & p . 16 = r . 4 & p . 17 = r . 26 & p . 18 = r . 8 & p . 19 = r . 16 & p . 20 = r . 7 & p . 21 = r . 27 & p . 22 = r . 20 & p . 23 = r . 13 & p . 24 = r . 2 & p . 25 = r . 41 & p . 26 = r . 52 & p . 27 = r . 31 & p . 28 = r . 37 & p . 29 = r . 47 & p . 30 = r . 55 & p . 31 = r . 30 & p . 32 = r . 40 & p . 33 = r . 51 & p . 34 = r . 45 & p . 35 = r . 33 & p . 36 = r . 48 & p . 37 = r . 44 & p . 38 = r . 49 & p . 39 = r . 39 & p . 40 = r . 56 & p . 41 = r . 34 & p . 42 = r . 53 & p . 43 = r . 46 & p . 44 = r . 42 & p . 45 = r . 50 & p . 46 = r . 36 & p . 47 = r . 29 & p . 48 = r . 32 & q . 1 = r . 14 & q . 2 = r . 17 & q . 3 = r . 11 & q . 4 = r . 24 & q . 5 = r . 1 & q . 6 = r . 5 & q . 7 = r . 3 & q . 8 = r . 28 & q . 9 = r . 15 & q . 10 = r . 6 & q . 11 = r . 21 & q . 12 = r . 10 & q . 13 = r . 23 & q . 14 = r . 19 & q . 15 = r . 12 & q . 16 = r . 4 & q . 17 = r . 26 & q . 18 = r . 8 & q . 19 = r . 16 & q . 20 = r . 7 & q . 21 = r . 27 & q . 22 = r . 20 & q . 23 = r . 13 & q . 24 = r . 2 & q . 25 = r . 41 & q . 26 = r . 52 & q . 27 = r . 31 & q . 28 = r . 37 & q . 29 = r . 47 & q . 30 = r . 55 & q . 31 = r . 30 & q . 32 = r . 40 & q . 33 = r . 51 & q . 34 = r . 45 & q . 35 = r . 33 & q . 36 = r . 48 & q . 37 = r . 44 & q . 38 = r . 49 & q . 39 = r . 39 & q . 40 = r . 56 & q . 41 = r . 34 & q . 42 = r . 53 & q . 43 = r . 46 & q . 44 = r . 42 & q . 45 = r . 50 & q . 46 = r . 36 & q . 47 = r . 29 & q . 48 = r . 32 implies p = q )
assume A2:
( p . 1 = r . 14 & p . 2 = r . 17 & p . 3 = r . 11 & p . 4 = r . 24 & p . 5 = r . 1 & p . 6 = r . 5 & p . 7 = r . 3 & p . 8 = r . 28 & p . 9 = r . 15 & p . 10 = r . 6 & p . 11 = r . 21 & p . 12 = r . 10 & p . 13 = r . 23 & p . 14 = r . 19 & p . 15 = r . 12 & p . 16 = r . 4 & p . 17 = r . 26 & p . 18 = r . 8 & p . 19 = r . 16 & p . 20 = r . 7 & p . 21 = r . 27 & p . 22 = r . 20 & p . 23 = r . 13 & p . 24 = r . 2 & p . 25 = r . 41 & p . 26 = r . 52 & p . 27 = r . 31 & p . 28 = r . 37 & p . 29 = r . 47 & p . 30 = r . 55 & p . 31 = r . 30 & p . 32 = r . 40 & p . 33 = r . 51 & p . 34 = r . 45 & p . 35 = r . 33 & p . 36 = r . 48 & p . 37 = r . 44 & p . 38 = r . 49 & p . 39 = r . 39 & p . 40 = r . 56 & p . 41 = r . 34 & p . 42 = r . 53 & p . 43 = r . 46 & p . 44 = r . 42 & p . 45 = r . 50 & p . 46 = r . 36 & p . 47 = r . 29 & p . 48 = r . 32 )
; ( not q . 1 = r . 14 or not q . 2 = r . 17 or not q . 3 = r . 11 or not q . 4 = r . 24 or not q . 5 = r . 1 or not q . 6 = r . 5 or not q . 7 = r . 3 or not q . 8 = r . 28 or not q . 9 = r . 15 or not q . 10 = r . 6 or not q . 11 = r . 21 or not q . 12 = r . 10 or not q . 13 = r . 23 or not q . 14 = r . 19 or not q . 15 = r . 12 or not q . 16 = r . 4 or not q . 17 = r . 26 or not q . 18 = r . 8 or not q . 19 = r . 16 or not q . 20 = r . 7 or not q . 21 = r . 27 or not q . 22 = r . 20 or not q . 23 = r . 13 or not q . 24 = r . 2 or not q . 25 = r . 41 or not q . 26 = r . 52 or not q . 27 = r . 31 or not q . 28 = r . 37 or not q . 29 = r . 47 or not q . 30 = r . 55 or not q . 31 = r . 30 or not q . 32 = r . 40 or not q . 33 = r . 51 or not q . 34 = r . 45 or not q . 35 = r . 33 or not q . 36 = r . 48 or not q . 37 = r . 44 or not q . 38 = r . 49 or not q . 39 = r . 39 or not q . 40 = r . 56 or not q . 41 = r . 34 or not q . 42 = r . 53 or not q . 43 = r . 46 or not q . 44 = r . 42 or not q . 45 = r . 50 or not q . 46 = r . 36 or not q . 47 = r . 29 or not q . 48 = r . 32 or p = q )
assume A3:
( q . 1 = r . 14 & q . 2 = r . 17 & q . 3 = r . 11 & q . 4 = r . 24 & q . 5 = r . 1 & q . 6 = r . 5 & q . 7 = r . 3 & q . 8 = r . 28 & q . 9 = r . 15 & q . 10 = r . 6 & q . 11 = r . 21 & q . 12 = r . 10 & q . 13 = r . 23 & q . 14 = r . 19 & q . 15 = r . 12 & q . 16 = r . 4 & q . 17 = r . 26 & q . 18 = r . 8 & q . 19 = r . 16 & q . 20 = r . 7 & q . 21 = r . 27 & q . 22 = r . 20 & q . 23 = r . 13 & q . 24 = r . 2 & q . 25 = r . 41 & q . 26 = r . 52 & q . 27 = r . 31 & q . 28 = r . 37 & q . 29 = r . 47 & q . 30 = r . 55 & q . 31 = r . 30 & q . 32 = r . 40 & q . 33 = r . 51 & q . 34 = r . 45 & q . 35 = r . 33 & q . 36 = r . 48 & q . 37 = r . 44 & q . 38 = r . 49 & q . 39 = r . 39 & q . 40 = r . 56 & q . 41 = r . 34 & q . 42 = r . 53 & q . 43 = r . 46 & q . 44 = r . 42 & q . 45 = r . 50 & q . 46 = r . 36 & q . 47 = r . 29 & q . 48 = r . 32 )
; p = q
p in { s where s is Element of BOOLEAN * : len s = 48 }
;
then consider t being Element of BOOLEAN * such that
A4:
( p = t & len t = 48 )
;
q in { s where s is Element of BOOLEAN * : len s = 48 }
;
then consider s being Element of BOOLEAN * such that
A5:
( q = s & len s = 48 )
;
A6:
( dom p = Seg 48 & dom q = Seg 48 )
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