theorem :: FINSEQ_3:121

for D being non empty set holds ExtendRel (id D) = id (D *)