let z be set ; :: thesis: <*z*> * <*1*> = <*z*>
A1: dom <*1*> = Seg 1 by FINSEQ_1:55;
A2: rng <*1*> = {1} by FINSEQ_1:55;
( dom <*z*> = Seg 1 & rng <*z*> = {z} ) by FINSEQ_1:55;
then A3: dom (<*z*> * <*1*>) = dom <*1*> by A2, FINSEQ_1:4, RELAT_1:46;
1 in dom <*1*> by A1, FINSEQ_1:4, TARSKI:def 1;
then (<*z*> * <*1*>) . 1 = <*z*> . (<*1*> . 1) by FUNCT_1:23
.= <*z*> . 1 by FINSEQ_1:57
.= z by FINSEQ_1:57 ;
hence <*z*> * <*1*> = <*z*> by A1, A3, FINSEQ_1:def 8; :: thesis: verum