set x0 = <*FALSE,FALSE,FALSE,FALSE*>;
set x1 = <*FALSE,FALSE,FALSE,TRUE*>;
set x2 = <*FALSE,FALSE,TRUE,FALSE*>;
set x3 = <*FALSE,FALSE,TRUE,TRUE*>;
set x4 = <*FALSE,TRUE,FALSE,FALSE*>;
set x5 = <*FALSE,TRUE,FALSE,TRUE*>;
set x6 = <*FALSE,TRUE,TRUE,FALSE*>;
set x7 = <*FALSE,TRUE,TRUE,TRUE*>;
set x8 = <*TRUE,FALSE,FALSE,FALSE*>;
set x9 = <*TRUE,FALSE,FALSE,TRUE*>;
set x10 = <*TRUE,FALSE,TRUE,FALSE*>;
set x11 = <*TRUE,FALSE,TRUE,TRUE*>;
set x12 = <*TRUE,TRUE,FALSE,FALSE*>;
set x13 = <*TRUE,TRUE,FALSE,TRUE*>;
set x14 = <*TRUE,TRUE,TRUE,FALSE*>;
set x15 = <*TRUE,TRUE,TRUE,TRUE*>;
L1: ( len <*FALSE,FALSE,FALSE,FALSE*> = 4 & len <*FALSE,FALSE,FALSE,TRUE*> = 4 & len <*FALSE,FALSE,TRUE,FALSE*> = 4 & len <*FALSE,FALSE,TRUE,TRUE*> = 4 & len <*FALSE,TRUE,FALSE,FALSE*> = 4 & len <*FALSE,TRUE,FALSE,TRUE*> = 4 & len <*FALSE,TRUE,TRUE,FALSE*> = 4 & len <*FALSE,TRUE,TRUE,TRUE*> = 4 & len <*TRUE,FALSE,FALSE,FALSE*> = 4 & len <*TRUE,FALSE,FALSE,TRUE*> = 4 & len <*TRUE,FALSE,TRUE,FALSE*> = 4 & len <*TRUE,FALSE,TRUE,TRUE*> = 4 & len <*TRUE,TRUE,FALSE,FALSE*> = 4 & len <*TRUE,TRUE,FALSE,TRUE*> = 4 & len <*TRUE,TRUE,TRUE,FALSE*> = 4 & len <*TRUE,TRUE,TRUE,TRUE*> = 4 ) by FINSEQ_4:76;
then reconsider x0 = <*FALSE,FALSE,FALSE,FALSE*> as Element of 4 -tuples_on BOOLEAN by FINSEQ_2:92;
reconsider x1 = <*FALSE,FALSE,FALSE,TRUE*> as Element of 4 -tuples_on BOOLEAN by L1, FINSEQ_2:92;
reconsider x2 = <*FALSE,FALSE,TRUE,FALSE*> as Element of 4 -tuples_on BOOLEAN by L1, FINSEQ_2:92;
reconsider x3 = <*FALSE,FALSE,TRUE,TRUE*> as Element of 4 -tuples_on BOOLEAN by L1, FINSEQ_2:92;
reconsider x4 = <*FALSE,TRUE,FALSE,FALSE*> as Element of 4 -tuples_on BOOLEAN by L1, FINSEQ_2:92;
reconsider x5 = <*FALSE,TRUE,FALSE,TRUE*> as Element of 4 -tuples_on BOOLEAN by L1, FINSEQ_2:92;
reconsider x6 = <*FALSE,TRUE,TRUE,FALSE*> as Element of 4 -tuples_on BOOLEAN by L1, FINSEQ_2:92;
reconsider x7 = <*FALSE,TRUE,TRUE,TRUE*> as Element of 4 -tuples_on BOOLEAN by L1, FINSEQ_2:92;
reconsider x8 = <*TRUE,FALSE,FALSE,FALSE*> as Element of 4 -tuples_on BOOLEAN by L1, FINSEQ_2:92;
reconsider x9 = <*TRUE,FALSE,FALSE,TRUE*> as Element of 4 -tuples_on BOOLEAN by L1, FINSEQ_2:92;
reconsider x10 = <*TRUE,FALSE,TRUE,FALSE*> as Element of 4 -tuples_on BOOLEAN by L1, FINSEQ_2:92;
reconsider x11 = <*TRUE,FALSE,TRUE,TRUE*> as Element of 4 -tuples_on BOOLEAN by L1, FINSEQ_2:92;
reconsider x12 = <*TRUE,TRUE,FALSE,FALSE*> as Element of 4 -tuples_on BOOLEAN by L1, FINSEQ_2:92;
reconsider x13 = <*TRUE,TRUE,FALSE,TRUE*> as Element of 4 -tuples_on BOOLEAN by L1, FINSEQ_2:92;
reconsider x14 = <*TRUE,TRUE,TRUE,FALSE*> as Element of 4 -tuples_on BOOLEAN by L1, FINSEQ_2:92;
reconsider x15 = <*TRUE,TRUE,TRUE,TRUE*> as Element of 4 -tuples_on BOOLEAN by L1, FINSEQ_2:92;
consider s being FinSequence of 4 -tuples_on BOOLEAN such that
LCS: ( s is 16 -element & s . 1 = x0 & s . 2 = x1 & s . 3 = x2 & s . 4 = x3 & s . 5 = x4 & s . 6 = x5 & s . 7 = x6 & s . 8 = x7 & s . 9 = x8 & s . 10 = x9 & s . 11 = x10 & s . 12 = x11 & s . 13 = x12 & s . 14 = x13 & s . 15 = x14 & s . 16 = x15 ) by TT16;
L2: len s = 16 by LCS, CARD_1:def 7;
set f = the NtoSEG Function of 16,(Seg 16);
rng the NtoSEG Function of 16,(Seg 16) = Seg 16 by FUNCT_2:def 3;
then the NtoSEG Function of 16,(Seg 16) " (dom s) = the NtoSEG Function of 16,(Seg 16) " (rng the NtoSEG Function of 16,(Seg 16)) by L2, FINSEQ_1:def 3
.= dom the NtoSEG Function of 16,(Seg 16) by RELAT_1:134 ;
then (dom the NtoSEG Function of 16,(Seg 16)) /\ ( the NtoSEG Function of 16,(Seg 16) " (dom s)) = dom the NtoSEG Function of 16,(Seg 16) ;
then LS5: dom (s * the NtoSEG Function of 16,(Seg 16)) = dom the NtoSEG Function of 16,(Seg 16) by EUCLID_7:1
.= 16 by FUNCT_2:def 1 ;
LS4: rng (s * the NtoSEG Function of 16,(Seg 16)) c= 4 -tuples_on BOOLEAN ;
reconsider s = s as Element of 16 -tuples_on (4 -tuples_on BOOLEAN) by L2, FINSEQ_2:92;
reconsider sf = s * the NtoSEG Function of 16,(Seg 16) as Function of 16,(4 -tuples_on BOOLEAN) by LS5, LS4, FUNCT_2:2;
take sf ; :: thesis: ( sf . 0 = <*0,0,0,0*> & sf . 1 = <*0,0,0,1*> & sf . 2 = <*0,0,1,0*> & sf . 3 = <*0,0,1,1*> & sf . 4 = <*0,1,0,0*> & sf . 5 = <*0,1,0,1*> & sf . 6 = <*0,1,1,0*> & sf . 7 = <*0,1,1,1*> & sf . 8 = <*1,0,0,0*> & sf . 9 = <*1,0,0,1*> & sf . 10 = <*1,0,1,0*> & sf . 11 = <*1,0,1,1*> & sf . 12 = <*1,1,0,0*> & sf . 13 = <*1,1,0,1*> & sf . 14 = <*1,1,1,0*> & sf . 15 = <*1,1,1,1*> )
thus ( sf . 0 = <*0,0,0,0*> & sf . 1 = <*0,0,0,1*> & sf . 2 = <*0,0,1,0*> & sf . 3 = <*0,0,1,1*> & sf . 4 = <*0,1,0,0*> & sf . 5 = <*0,1,0,1*> & sf . 6 = <*0,1,1,0*> & sf . 7 = <*0,1,1,1*> & sf . 8 = <*1,0,0,0*> & sf . 9 = <*1,0,0,1*> & sf . 10 = <*1,0,1,0*> & sf . 11 = <*1,0,1,1*> & sf . 12 = <*1,1,0,0*> & sf . 13 = <*1,1,0,1*> & sf . 14 = <*1,1,1,0*> & sf . 15 = <*1,1,1,1*> ) by ThL2L16, LCS; :: thesis: verum