let S be non empty set ; for x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26, x27, x28, x29, x30, x31, x32, x33, x34, x35, x36, x37, x38, x39, x40, x41, x42, x43, x44, x45, x46, x47, x48, x49, x50, x51, x52, x53, x54, x55, x56, x57, x58, x59, x60, x61, x62, x63, x64 being Element of S ex f being Function of 64,S st
( f . 0 = x1 & f . 1 = x2 & f . 2 = x3 & f . 3 = x4 & f . 4 = x5 & f . 5 = x6 & f . 6 = x7 & f . 7 = x8 & f . 8 = x9 & f . 9 = x10 & f . 10 = x11 & f . 11 = x12 & f . 12 = x13 & f . 13 = x14 & f . 14 = x15 & f . 15 = x16 & f . 16 = x17 & f . 17 = x18 & f . 18 = x19 & f . 19 = x20 & f . 20 = x21 & f . 21 = x22 & f . 22 = x23 & f . 23 = x24 & f . 24 = x25 & f . 25 = x26 & f . 26 = x27 & f . 27 = x28 & f . 28 = x29 & f . 29 = x30 & f . 30 = x31 & f . 31 = x32 & f . 32 = x33 & f . 33 = x34 & f . 34 = x35 & f . 35 = x36 & f . 36 = x37 & f . 37 = x38 & f . 38 = x39 & f . 39 = x40 & f . 40 = x41 & f . 41 = x42 & f . 42 = x43 & f . 43 = x44 & f . 44 = x45 & f . 45 = x46 & f . 46 = x47 & f . 47 = x48 & f . 48 = x49 & f . 49 = x50 & f . 50 = x51 & f . 51 = x52 & f . 52 = x53 & f . 53 = x54 & f . 54 = x55 & f . 55 = x56 & f . 56 = x57 & f . 57 = x58 & f . 58 = x59 & f . 59 = x60 & f . 60 = x61 & f . 61 = x62 & f . 62 = x63 & f . 63 = x64 )
let x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26, x27, x28, x29, x30, x31, x32, x33, x34, x35, x36, x37, x38, x39, x40, x41, x42, x43, x44, x45, x46, x47, x48, x49, x50, x51, x52, x53, x54, x55, x56, x57, x58, x59, x60, x61, x62, x63, x64 be Element of S; ex f being Function of 64,S st
( f . 0 = x1 & f . 1 = x2 & f . 2 = x3 & f . 3 = x4 & f . 4 = x5 & f . 5 = x6 & f . 6 = x7 & f . 7 = x8 & f . 8 = x9 & f . 9 = x10 & f . 10 = x11 & f . 11 = x12 & f . 12 = x13 & f . 13 = x14 & f . 14 = x15 & f . 15 = x16 & f . 16 = x17 & f . 17 = x18 & f . 18 = x19 & f . 19 = x20 & f . 20 = x21 & f . 21 = x22 & f . 22 = x23 & f . 23 = x24 & f . 24 = x25 & f . 25 = x26 & f . 26 = x27 & f . 27 = x28 & f . 28 = x29 & f . 29 = x30 & f . 30 = x31 & f . 31 = x32 & f . 32 = x33 & f . 33 = x34 & f . 34 = x35 & f . 35 = x36 & f . 36 = x37 & f . 37 = x38 & f . 38 = x39 & f . 39 = x40 & f . 40 = x41 & f . 41 = x42 & f . 42 = x43 & f . 43 = x44 & f . 44 = x45 & f . 45 = x46 & f . 46 = x47 & f . 47 = x48 & f . 48 = x49 & f . 49 = x50 & f . 50 = x51 & f . 51 = x52 & f . 52 = x53 & f . 53 = x54 & f . 54 = x55 & f . 55 = x56 & f . 56 = x57 & f . 57 = x58 & f . 58 = x59 & f . 59 = x60 & f . 60 = x61 & f . 61 = x62 & f . 62 = x63 & f . 63 = x64 )
consider t being FinSequence of S such that
A1:
( t is 64 -element & t . 1 = x1 & t . 2 = x2 & t . 3 = x3 & t . 4 = x4 & t . 5 = x5 & t . 6 = x6 & t . 7 = x7 & t . 8 = x8 & t . 9 = x9 & t . 10 = x10 & t . 11 = x11 & t . 12 = x12 & t . 13 = x13 & t . 14 = x14 & t . 15 = x15 & t . 16 = x16 & t . 17 = x17 & t . 18 = x18 & t . 19 = x19 & t . 20 = x20 & t . 21 = x21 & t . 22 = x22 & t . 23 = x23 & t . 24 = x24 & t . 25 = x25 & t . 26 = x26 & t . 27 = x27 & t . 28 = x28 & t . 29 = x29 & t . 30 = x30 & t . 31 = x31 & t . 32 = x32 & t . 33 = x33 & t . 34 = x34 & t . 35 = x35 & t . 36 = x36 & t . 37 = x37 & t . 38 = x38 & t . 39 = x39 & t . 40 = x40 & t . 41 = x41 & t . 42 = x42 & t . 43 = x43 & t . 44 = x44 & t . 45 = x45 & t . 46 = x46 & t . 47 = x47 & t . 48 = x48 & t . 49 = x49 & t . 50 = x50 & t . 51 = x51 & t . 52 = x52 & t . 53 = x53 & t . 54 = x54 & t . 55 = x55 & t . 56 = x56 & t . 57 = x57 & t . 58 = x58 & t . 59 = x59 & t . 60 = x60 & t . 61 = x61 & t . 62 = x62 & t . 63 = x63 & t . 64 = x64 )
by Th25;
A2:
len t = 64
by A1;
set f = the NtoSEG Function of (Segm 64),(Seg 64);
rng the NtoSEG Function of (Segm 64),(Seg 64) = Seg 64
by FUNCT_2:def 3;
then the NtoSEG Function of (Segm 64),(Seg 64) " (dom t) =
the NtoSEG Function of (Segm 64),(Seg 64) " (rng the NtoSEG Function of (Segm 64),(Seg 64))
by A2, FINSEQ_1:def 3
.=
dom the NtoSEG Function of (Segm 64),(Seg 64)
by RELAT_1:134
;
then A3: dom (t * the NtoSEG Function of (Segm 64),(Seg 64)) =
dom the NtoSEG Function of (Segm 64),(Seg 64)
by RELAT_1:147
.=
64
by FUNCT_2:def 1
;
A4:
rng (t * the NtoSEG Function of (Segm 64),(Seg 64)) c= S
;
reconsider t = t as Element of 64 -tuples_on S by A2, FINSEQ_2:92;
reconsider tf = t * the NtoSEG Function of (Segm 64),(Seg 64) as Function of 64,S by A3, A4, FUNCT_2:2;
take
tf
; ( tf . 0 = x1 & tf . 1 = x2 & tf . 2 = x3 & tf . 3 = x4 & tf . 4 = x5 & tf . 5 = x6 & tf . 6 = x7 & tf . 7 = x8 & tf . 8 = x9 & tf . 9 = x10 & tf . 10 = x11 & tf . 11 = x12 & tf . 12 = x13 & tf . 13 = x14 & tf . 14 = x15 & tf . 15 = x16 & tf . 16 = x17 & tf . 17 = x18 & tf . 18 = x19 & tf . 19 = x20 & tf . 20 = x21 & tf . 21 = x22 & tf . 22 = x23 & tf . 23 = x24 & tf . 24 = x25 & tf . 25 = x26 & tf . 26 = x27 & tf . 27 = x28 & tf . 28 = x29 & tf . 29 = x30 & tf . 30 = x31 & tf . 31 = x32 & tf . 32 = x33 & tf . 33 = x34 & tf . 34 = x35 & tf . 35 = x36 & tf . 36 = x37 & tf . 37 = x38 & tf . 38 = x39 & tf . 39 = x40 & tf . 40 = x41 & tf . 41 = x42 & tf . 42 = x43 & tf . 43 = x44 & tf . 44 = x45 & tf . 45 = x46 & tf . 46 = x47 & tf . 47 = x48 & tf . 48 = x49 & tf . 49 = x50 & tf . 50 = x51 & tf . 51 = x52 & tf . 52 = x53 & tf . 53 = x54 & tf . 54 = x55 & tf . 55 = x56 & tf . 56 = x57 & tf . 57 = x58 & tf . 58 = x59 & tf . 59 = x60 & tf . 60 = x61 & tf . 61 = x62 & tf . 62 = x63 & tf . 63 = x64 )
thus
( tf . 0 = x1 & tf . 1 = x2 & tf . 2 = x3 & tf . 3 = x4 & tf . 4 = x5 & tf . 5 = x6 & tf . 6 = x7 & tf . 7 = x8 & tf . 8 = x9 & tf . 9 = x10 & tf . 10 = x11 & tf . 11 = x12 & tf . 12 = x13 & tf . 13 = x14 & tf . 14 = x15 & tf . 15 = x16 & tf . 16 = x17 & tf . 17 = x18 & tf . 18 = x19 & tf . 19 = x20 & tf . 20 = x21 & tf . 21 = x22 & tf . 22 = x23 & tf . 23 = x24 & tf . 24 = x25 & tf . 25 = x26 & tf . 26 = x27 & tf . 27 = x28 & tf . 28 = x29 & tf . 29 = x30 & tf . 30 = x31 & tf . 31 = x32 & tf . 32 = x33 & tf . 33 = x34 & tf . 34 = x35 & tf . 35 = x36 & tf . 36 = x37 & tf . 37 = x38 & tf . 38 = x39 & tf . 39 = x40 & tf . 40 = x41 & tf . 41 = x42 & tf . 42 = x43 & tf . 43 = x44 & tf . 44 = x45 & tf . 45 = x46 & tf . 46 = x47 & tf . 47 = x48 & tf . 48 = x49 & tf . 49 = x50 & tf . 50 = x51 & tf . 51 = x52 & tf . 52 = x53 & tf . 53 = x54 & tf . 54 = x55 & tf . 55 = x56 & tf . 56 = x57 & tf . 57 = x58 & tf . 58 = x59 & tf . 59 = x60 & tf . 60 = x61 & tf . 61 = x62 & tf . 62 = x63 & tf . 63 = x64 )
by A1, Lm2; verum