let z be set ; :: thesis: <*z*> * <*1*> = <*z*>
A1: dom <*z*> = Seg 1 by FINSEQ_1:38;
rng <*1*> = {1} by FINSEQ_1:38;
then A2: dom (<*z*> * <*1*>) = dom <*1*> by A1, FINSEQ_1:2, RELAT_1:27;
A3: dom <*1*> = Seg 1 by FINSEQ_1:38;
then 1 in dom <*1*> by FINSEQ_1:2, TARSKI:def 1;
then (<*z*> * <*1*>) . 1 = <*z*> . (<*1*> . 1) by FUNCT_1:13
.= <*z*> . 1
.= z ;
hence <*z*> * <*1*> = <*z*> by A3, A2, FINSEQ_1:def 8; :: thesis: verum