let x, y be set ; :: thesis: ( not <*x*> is empty & not <*x,y*> is empty )
( len <*x*> = 1 & len <*x,y*> = 2 ) by FINSEQ_1:57, FINSEQ_1:61;
then ( dom <*x*> = Seg 1 & dom <*x,y*> = Seg 2 & 1 in Seg 1 & 1 in Seg 2 & <*x*> = <*x*> & <*x,y*> = <*x,y*> ) by FINSEQ_1:4, FINSEQ_1:def 3, TARSKI:def 1, TARSKI:def 2;
then ( [1,(<*x*> . 1)] in <*x*> & [1,(<*x,y*> . 1)] in <*x,y*> ) by FUNCT_1:8;
hence ( not <*x*> is empty & not <*x,y*> is empty ) ; :: thesis: verum