let f be NtoSEG Function of 16,(Seg 16); :: thesis:
let S be non empty set ; :: thesis:
let x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16 be Element of S; :: thesis:
let t be Element of 16 -tuples_on S; :: thesis:
assume ( 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 ) ; :: thesis:
then ( t . (0 + 1) = x1 & t . (1 + 1) = x2 & t . (2 + 1) = x3 & t . (3 + 1) = x4 & t . (4 + 1) = x5 & t . (5 + 1) = x6 & t . (6 + 1) = x7 & t . (7 + 1) = x8 & t . (8 + 1) = x9 & t . (9 + 1) = x10 & t . (10 + 1) = x11 & t . (11 + 1) = x12 & t . (12 + 1) = x13 & t . (13 + 1) = x14 & t . (14 + 1) = x15 & t . (15 + 1) = x16 ) ;
then L1: ( t . (f . 0) = x1 & t . (f . 1) = x2 & t . (f . 2) = x3 & t . (f . 3) = x4 & t . (f . 4) = x5 & t . (f . 5) = x6 & t . (f . 6) = x7 & t . (f . 7) = x8 & t . (f . 8) = x9 & t . (f . 9) = x10 & t . (f . 10) = x11 & t . (f . 11) = x12 & t . (f . 12) = x13 & t . (f . 13) = x14 & t . (f . 14) = x15 & t . (f . 15) = x16 ) by ThL1;
( 0 in dom f & 1 in dom f & 2 in dom f & 3 in dom f & 4 in dom f & 5 in dom f & 6 in dom f & 7 in dom f & 8 in dom f & 9 in dom f & 10 in dom f & 11 in dom f & 12 in dom f & 13 in dom f & 14 in dom f & 15 in dom f ) by ThL1;
hence ( (t * f) . 0 = x1 & (t * f) . 1 = x2 & (t * f) . 2 = x3 & (t * f) . 3 = x4 & (t * f) . 4 = x5 & (t * f) . 5 = x6 & (t * f) . 6 = x7 & (t * f) . 7 = x8 & (t * f) . 8 = x9 & (t * f) . 9 = x10 & (t * f) . 10 = x11 & (t * f) . 11 = x12 & (t * f) . 12 = x13 & (t * f) . 13 = x14 & (t * f) . 14 = x15 & (t * f) . 15 = x16 ) by L1, FUNCT_1:13; :: thesis: