let A be set ; :: thesis: delta A = <:(id A),(id A):>
thus delta A = (id [:A,A:]) * (delta A) by FUNCT_2:17
.= [:(id A),(id A):] * (delta A) by FUNCT_3:69
.= <:(id A),(id A):> by FUNCT_3:78 ; :: thesis: verum