take A ; :: thesis: ex f being Permutation of (dom A) st A = A * f
take id (dom A) ; :: thesis: A = A * (id (dom A))
thus A = A * (id (dom A)) by RELAT_1:51; :: thesis: verum