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 16; for f, g being Function of 64,16 st f . 1 = x1 & f . 2 = x2 & f . 3 = x3 & f . 4 = x4 & f . 5 = x5 & f . 6 = x6 & f . 7 = x7 & f . 8 = x8 & f . 9 = x9 & f . 10 = x10 & f . 11 = x11 & f . 12 = x12 & f . 13 = x13 & f . 14 = x14 & f . 15 = x15 & f . 16 = x16 & f . 17 = x17 & f . 18 = x18 & f . 19 = x19 & f . 20 = x20 & f . 21 = x21 & f . 22 = x22 & f . 23 = x23 & f . 24 = x24 & f . 25 = x25 & f . 26 = x26 & f . 27 = x27 & f . 28 = x28 & f . 29 = x29 & f . 30 = x30 & f . 31 = x31 & f . 32 = x32 & f . 33 = x33 & f . 34 = x34 & f . 35 = x35 & f . 36 = x36 & f . 37 = x37 & f . 38 = x38 & f . 39 = x39 & f . 40 = x40 & f . 41 = x41 & f . 42 = x42 & f . 43 = x43 & f . 44 = x44 & f . 45 = x45 & f . 46 = x46 & f . 47 = x47 & f . 48 = x48 & f . 49 = x49 & f . 50 = x50 & f . 51 = x51 & f . 52 = x52 & f . 53 = x53 & f . 54 = x54 & f . 55 = x55 & f . 56 = x56 & f . 57 = x57 & f . 58 = x58 & f . 59 = x59 & f . 60 = x60 & f . 61 = x61 & f . 62 = x62 & f . 63 = x63 & f . 0 = x64 & g . 1 = x1 & g . 2 = x2 & g . 3 = x3 & g . 4 = x4 & g . 5 = x5 & g . 6 = x6 & g . 7 = x7 & g . 8 = x8 & g . 9 = x9 & g . 10 = x10 & g . 11 = x11 & g . 12 = x12 & g . 13 = x13 & g . 14 = x14 & g . 15 = x15 & g . 16 = x16 & g . 17 = x17 & g . 18 = x18 & g . 19 = x19 & g . 20 = x20 & g . 21 = x21 & g . 22 = x22 & g . 23 = x23 & g . 24 = x24 & g . 25 = x25 & g . 26 = x26 & g . 27 = x27 & g . 28 = x28 & g . 29 = x29 & g . 30 = x30 & g . 31 = x31 & g . 32 = x32 & g . 33 = x33 & g . 34 = x34 & g . 35 = x35 & g . 36 = x36 & g . 37 = x37 & g . 38 = x38 & g . 39 = x39 & g . 40 = x40 & g . 41 = x41 & g . 42 = x42 & g . 43 = x43 & g . 44 = x44 & g . 45 = x45 & g . 46 = x46 & g . 47 = x47 & g . 48 = x48 & g . 49 = x49 & g . 50 = x50 & g . 51 = x51 & g . 52 = x52 & g . 53 = x53 & g . 54 = x54 & g . 55 = x55 & g . 56 = x56 & g . 57 = x57 & g . 58 = x58 & g . 59 = x59 & g . 60 = x60 & g . 61 = x61 & g . 62 = x62 & g . 63 = x63 & g . 0 = x64 holds
f = g
let f, g be Function of 64,16; ( f . 1 = x1 & f . 2 = x2 & f . 3 = x3 & f . 4 = x4 & f . 5 = x5 & f . 6 = x6 & f . 7 = x7 & f . 8 = x8 & f . 9 = x9 & f . 10 = x10 & f . 11 = x11 & f . 12 = x12 & f . 13 = x13 & f . 14 = x14 & f . 15 = x15 & f . 16 = x16 & f . 17 = x17 & f . 18 = x18 & f . 19 = x19 & f . 20 = x20 & f . 21 = x21 & f . 22 = x22 & f . 23 = x23 & f . 24 = x24 & f . 25 = x25 & f . 26 = x26 & f . 27 = x27 & f . 28 = x28 & f . 29 = x29 & f . 30 = x30 & f . 31 = x31 & f . 32 = x32 & f . 33 = x33 & f . 34 = x34 & f . 35 = x35 & f . 36 = x36 & f . 37 = x37 & f . 38 = x38 & f . 39 = x39 & f . 40 = x40 & f . 41 = x41 & f . 42 = x42 & f . 43 = x43 & f . 44 = x44 & f . 45 = x45 & f . 46 = x46 & f . 47 = x47 & f . 48 = x48 & f . 49 = x49 & f . 50 = x50 & f . 51 = x51 & f . 52 = x52 & f . 53 = x53 & f . 54 = x54 & f . 55 = x55 & f . 56 = x56 & f . 57 = x57 & f . 58 = x58 & f . 59 = x59 & f . 60 = x60 & f . 61 = x61 & f . 62 = x62 & f . 63 = x63 & f . 0 = x64 & g . 1 = x1 & g . 2 = x2 & g . 3 = x3 & g . 4 = x4 & g . 5 = x5 & g . 6 = x6 & g . 7 = x7 & g . 8 = x8 & g . 9 = x9 & g . 10 = x10 & g . 11 = x11 & g . 12 = x12 & g . 13 = x13 & g . 14 = x14 & g . 15 = x15 & g . 16 = x16 & g . 17 = x17 & g . 18 = x18 & g . 19 = x19 & g . 20 = x20 & g . 21 = x21 & g . 22 = x22 & g . 23 = x23 & g . 24 = x24 & g . 25 = x25 & g . 26 = x26 & g . 27 = x27 & g . 28 = x28 & g . 29 = x29 & g . 30 = x30 & g . 31 = x31 & g . 32 = x32 & g . 33 = x33 & g . 34 = x34 & g . 35 = x35 & g . 36 = x36 & g . 37 = x37 & g . 38 = x38 & g . 39 = x39 & g . 40 = x40 & g . 41 = x41 & g . 42 = x42 & g . 43 = x43 & g . 44 = x44 & g . 45 = x45 & g . 46 = x46 & g . 47 = x47 & g . 48 = x48 & g . 49 = x49 & g . 50 = x50 & g . 51 = x51 & g . 52 = x52 & g . 53 = x53 & g . 54 = x54 & g . 55 = x55 & g . 56 = x56 & g . 57 = x57 & g . 58 = x58 & g . 59 = x59 & g . 60 = x60 & g . 61 = x61 & g . 62 = x62 & g . 63 = x63 & g . 0 = x64 implies f = g )
assume A1:
( f . 1 = x1 & f . 2 = x2 & f . 3 = x3 & f . 4 = x4 & f . 5 = x5 & f . 6 = x6 & f . 7 = x7 & f . 8 = x8 & f . 9 = x9 & f . 10 = x10 & f . 11 = x11 & f . 12 = x12 & f . 13 = x13 & f . 14 = x14 & f . 15 = x15 & f . 16 = x16 & f . 17 = x17 & f . 18 = x18 & f . 19 = x19 & f . 20 = x20 & f . 21 = x21 & f . 22 = x22 & f . 23 = x23 & f . 24 = x24 & f . 25 = x25 & f . 26 = x26 & f . 27 = x27 & f . 28 = x28 & f . 29 = x29 & f . 30 = x30 & f . 31 = x31 & f . 32 = x32 & f . 33 = x33 & f . 34 = x34 & f . 35 = x35 & f . 36 = x36 & f . 37 = x37 & f . 38 = x38 & f . 39 = x39 & f . 40 = x40 & f . 41 = x41 & f . 42 = x42 & f . 43 = x43 & f . 44 = x44 & f . 45 = x45 & f . 46 = x46 & f . 47 = x47 & f . 48 = x48 & f . 49 = x49 & f . 50 = x50 & f . 51 = x51 & f . 52 = x52 & f . 53 = x53 & f . 54 = x54 & f . 55 = x55 & f . 56 = x56 & f . 57 = x57 & f . 58 = x58 & f . 59 = x59 & f . 60 = x60 & f . 61 = x61 & f . 62 = x62 & f . 63 = x63 & f . 0 = x64 & g . 1 = x1 & g . 2 = x2 & g . 3 = x3 & g . 4 = x4 & g . 5 = x5 & g . 6 = x6 & g . 7 = x7 & g . 8 = x8 & g . 9 = x9 & g . 10 = x10 & g . 11 = x11 & g . 12 = x12 & g . 13 = x13 & g . 14 = x14 & g . 15 = x15 & g . 16 = x16 & g . 17 = x17 & g . 18 = x18 & g . 19 = x19 & g . 20 = x20 & g . 21 = x21 & g . 22 = x22 & g . 23 = x23 & g . 24 = x24 & g . 25 = x25 & g . 26 = x26 & g . 27 = x27 & g . 28 = x28 & g . 29 = x29 & g . 30 = x30 & g . 31 = x31 & g . 32 = x32 & g . 33 = x33 & g . 34 = x34 & g . 35 = x35 & g . 36 = x36 & g . 37 = x37 & g . 38 = x38 & g . 39 = x39 & g . 40 = x40 & g . 41 = x41 & g . 42 = x42 & g . 43 = x43 & g . 44 = x44 & g . 45 = x45 & g . 46 = x46 & g . 47 = x47 & g . 48 = x48 & g . 49 = x49 & g . 50 = x50 & g . 51 = x51 & g . 52 = x52 & g . 53 = x53 & g . 54 = x54 & g . 55 = x55 & g . 56 = x56 & g . 57 = x57 & g . 58 = x58 & g . 59 = x59 & g . 60 = x60 & g . 61 = x61 & g . 62 = x62 & g . 63 = x63 & g . 0 = x64 )
; f = g
A2:
( dom f = 63 + 1 & dom g = 64 )
by FUNCT_2:def 1;
for i being object st i in dom f holds
f . i = g . i
hence
f = g
by A2; verum