consider e being FinSequence of BOOLEAN such that
A1:
( e is 32 -element & e . 1 = r . 16 & e . 2 = r . 7 & e . 3 = r . 20 & e . 4 = r . 21 & e . 5 = r . 29 & e . 6 = r . 12 & e . 7 = r . 28 & e . 8 = r . 17 & e . 9 = r . 1 & e . 10 = r . 15 & e . 11 = r . 23 & e . 12 = r . 26 & e . 13 = r . 5 & e . 14 = r . 18 & e . 15 = r . 31 & e . 16 = r . 10 & e . 17 = r . 2 & e . 18 = r . 8 & e . 19 = r . 24 & e . 20 = r . 14 & e . 21 = r . 32 & e . 22 = r . 27 & e . 23 = r . 3 & e . 24 = r . 9 & e . 25 = r . 19 & e . 26 = r . 13 & e . 27 = r . 30 & e . 28 = r . 6 & e . 29 = r . 22 & e . 30 = r . 11 & e . 31 = r . 4 & e . 32 = r . 25 )
by Th22;
len e = 32
by A1;
then reconsider e = e as Element of 32 -tuples_on BOOLEAN by FINSEQ_2:92;
take
e
; ( e . 1 = r . 16 & e . 2 = r . 7 & e . 3 = r . 20 & e . 4 = r . 21 & e . 5 = r . 29 & e . 6 = r . 12 & e . 7 = r . 28 & e . 8 = r . 17 & e . 9 = r . 1 & e . 10 = r . 15 & e . 11 = r . 23 & e . 12 = r . 26 & e . 13 = r . 5 & e . 14 = r . 18 & e . 15 = r . 31 & e . 16 = r . 10 & e . 17 = r . 2 & e . 18 = r . 8 & e . 19 = r . 24 & e . 20 = r . 14 & e . 21 = r . 32 & e . 22 = r . 27 & e . 23 = r . 3 & e . 24 = r . 9 & e . 25 = r . 19 & e . 26 = r . 13 & e . 27 = r . 30 & e . 28 = r . 6 & e . 29 = r . 22 & e . 30 = r . 11 & e . 31 = r . 4 & e . 32 = r . 25 )
thus
( e . 1 = r . 16 & e . 2 = r . 7 & e . 3 = r . 20 & e . 4 = r . 21 & e . 5 = r . 29 & e . 6 = r . 12 & e . 7 = r . 28 & e . 8 = r . 17 & e . 9 = r . 1 & e . 10 = r . 15 & e . 11 = r . 23 & e . 12 = r . 26 & e . 13 = r . 5 & e . 14 = r . 18 & e . 15 = r . 31 & e . 16 = r . 10 & e . 17 = r . 2 & e . 18 = r . 8 & e . 19 = r . 24 & e . 20 = r . 14 & e . 21 = r . 32 & e . 22 = r . 27 & e . 23 = r . 3 & e . 24 = r . 9 & e . 25 = r . 19 & e . 26 = r . 13 & e . 27 = r . 30 & e . 28 = r . 6 & e . 29 = r . 22 & e . 30 = r . 11 & e . 31 = r . 4 & e . 32 = r . 25 )
by A1; verum