set P = IdPrefSpace A;
the carrier of (IdPrefSpace A) = A by Def5;
hence IdPrefSpace A is total by Def5; :: thesis: verum