ex g being Function st g * (Rel2Map L) = id (dom (Rel2Map L))

proof

take Map2Rel L ; :: thesis: (Map2Rel L) * (Rel2Map L) = id (dom (Rel2Map L))
thus (Map2Rel L) * (Rel2Map L) = id (dom (Rel2Map L)) by Th30; :: thesis: verum

end;

hence Rel2Map L is one-to-one by FUNCT_1:31; :: thesis: verum