consider e being FinSequence of BOOLEAN such that
A1:
( e is 64 -element & e . 1 = r . 40 & e . 2 = r . 8 & e . 3 = r . 48 & e . 4 = r . 16 & e . 5 = r . 56 & e . 6 = r . 24 & e . 7 = r . 64 & e . 8 = r . 32 & e . 9 = r . 39 & e . 10 = r . 7 & e . 11 = r . 47 & e . 12 = r . 15 & e . 13 = r . 55 & e . 14 = r . 23 & e . 15 = r . 63 & e . 16 = r . 31 & e . 17 = r . 38 & e . 18 = r . 6 & e . 19 = r . 46 & e . 20 = r . 14 & e . 21 = r . 54 & e . 22 = r . 22 & e . 23 = r . 62 & e . 24 = r . 30 & e . 25 = r . 37 & e . 26 = r . 5 & e . 27 = r . 45 & e . 28 = r . 13 & e . 29 = r . 53 & e . 30 = r . 21 & e . 31 = r . 61 & e . 32 = r . 29 & e . 33 = r . 36 & e . 34 = r . 4 & e . 35 = r . 44 & e . 36 = r . 12 & e . 37 = r . 52 & e . 38 = r . 20 & e . 39 = r . 60 & e . 40 = r . 28 & e . 41 = r . 35 & e . 42 = r . 3 & e . 43 = r . 43 & e . 44 = r . 11 & e . 45 = r . 51 & e . 46 = r . 19 & e . 47 = r . 59 & e . 48 = r . 27 & e . 49 = r . 34 & e . 50 = r . 2 & e . 51 = r . 42 & e . 52 = r . 10 & e . 53 = r . 50 & e . 54 = r . 18 & e . 55 = r . 58 & e . 56 = r . 26 & e . 57 = r . 33 & e . 58 = r . 1 & e . 59 = r . 41 & e . 60 = r . 9 & e . 61 = r . 49 & e . 62 = r . 17 & e . 63 = r . 57 & e . 64 = r . 25 )
by Th25;
len e = 64
by A1;
then reconsider e = e as Element of 64 -tuples_on BOOLEAN by FINSEQ_2:92;
take
e
; ( e . 1 = r . 40 & e . 2 = r . 8 & e . 3 = r . 48 & e . 4 = r . 16 & e . 5 = r . 56 & e . 6 = r . 24 & e . 7 = r . 64 & e . 8 = r . 32 & e . 9 = r . 39 & e . 10 = r . 7 & e . 11 = r . 47 & e . 12 = r . 15 & e . 13 = r . 55 & e . 14 = r . 23 & e . 15 = r . 63 & e . 16 = r . 31 & e . 17 = r . 38 & e . 18 = r . 6 & e . 19 = r . 46 & e . 20 = r . 14 & e . 21 = r . 54 & e . 22 = r . 22 & e . 23 = r . 62 & e . 24 = r . 30 & e . 25 = r . 37 & e . 26 = r . 5 & e . 27 = r . 45 & e . 28 = r . 13 & e . 29 = r . 53 & e . 30 = r . 21 & e . 31 = r . 61 & e . 32 = r . 29 & e . 33 = r . 36 & e . 34 = r . 4 & e . 35 = r . 44 & e . 36 = r . 12 & e . 37 = r . 52 & e . 38 = r . 20 & e . 39 = r . 60 & e . 40 = r . 28 & e . 41 = r . 35 & e . 42 = r . 3 & e . 43 = r . 43 & e . 44 = r . 11 & e . 45 = r . 51 & e . 46 = r . 19 & e . 47 = r . 59 & e . 48 = r . 27 & e . 49 = r . 34 & e . 50 = r . 2 & e . 51 = r . 42 & e . 52 = r . 10 & e . 53 = r . 50 & e . 54 = r . 18 & e . 55 = r . 58 & e . 56 = r . 26 & e . 57 = r . 33 & e . 58 = r . 1 & e . 59 = r . 41 & e . 60 = r . 9 & e . 61 = r . 49 & e . 62 = r . 17 & e . 63 = r . 57 & e . 64 = r . 25 )
thus
( e . 1 = r . 40 & e . 2 = r . 8 & e . 3 = r . 48 & e . 4 = r . 16 & e . 5 = r . 56 & e . 6 = r . 24 & e . 7 = r . 64 & e . 8 = r . 32 & e . 9 = r . 39 & e . 10 = r . 7 & e . 11 = r . 47 & e . 12 = r . 15 & e . 13 = r . 55 & e . 14 = r . 23 & e . 15 = r . 63 & e . 16 = r . 31 & e . 17 = r . 38 & e . 18 = r . 6 & e . 19 = r . 46 & e . 20 = r . 14 & e . 21 = r . 54 & e . 22 = r . 22 & e . 23 = r . 62 & e . 24 = r . 30 & e . 25 = r . 37 & e . 26 = r . 5 & e . 27 = r . 45 & e . 28 = r . 13 & e . 29 = r . 53 & e . 30 = r . 21 & e . 31 = r . 61 & e . 32 = r . 29 & e . 33 = r . 36 & e . 34 = r . 4 & e . 35 = r . 44 & e . 36 = r . 12 & e . 37 = r . 52 & e . 38 = r . 20 & e . 39 = r . 60 & e . 40 = r . 28 & e . 41 = r . 35 & e . 42 = r . 3 & e . 43 = r . 43 & e . 44 = r . 11 & e . 45 = r . 51 & e . 46 = r . 19 & e . 47 = r . 59 & e . 48 = r . 27 & e . 49 = r . 34 & e . 50 = r . 2 & e . 51 = r . 42 & e . 52 = r . 10 & e . 53 = r . 50 & e . 54 = r . 18 & e . 55 = r . 58 & e . 56 = r . 26 & e . 57 = r . 33 & e . 58 = r . 1 & e . 59 = r . 41 & e . 60 = r . 9 & e . 61 = r . 49 & e . 62 = r . 17 & e . 63 = r . 57 & e . 64 = r . 25 )
by A1; verum