let S be non empty set ; :: thesis: 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; :: thesis: 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
LCS: ( 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 TT64;
L2: len t = 64 by LCS, CARD_1:def 7;
set f = the NtoSEG Function of 64,(Seg 64);
rng the NtoSEG Function of 64,(Seg 64) = Seg 64 by FUNCT_2:def 3;
then the NtoSEG Function of 64,(Seg 64) " (dom t) = the NtoSEG Function of 64,(Seg 64) " (rng the NtoSEG Function of 64,(Seg 64)) by L2, FINSEQ_1:def 3
.= dom the NtoSEG Function of 64,(Seg 64) by RELAT_1:134 ;
then (dom the NtoSEG Function of 64,(Seg 64)) /\ ( the NtoSEG Function of 64,(Seg 64) " (dom t)) = dom the NtoSEG Function of 64,(Seg 64) ;
then LS5: dom (t * the NtoSEG Function of 64,(Seg 64)) = dom the NtoSEG Function of 64,(Seg 64) by EUCLID_7:1
.= 64 by FUNCT_2:def 1 ;
LS4: rng (t * the NtoSEG Function of 64,(Seg 64)) c= S ;
reconsider t = t as Element of 64 -tuples_on S by L2, FINSEQ_2:92;
reconsider tf = t * the NtoSEG Function of 64,(Seg 64) as Function of 64,S by LS5, LS4, FUNCT_2:2;
take tf ; :: thesis: ( 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 LCS, ThL2; :: thesis: verum