set f = IntMap T;
A2: (IntMap T) . ({} T) = Int ({} T) by Def16
.= {} T ;
(IntMap T) . ([#] T) = Int ([#] T) by Def16
.= [#] T by TOPS_1:15 ;
hence ( IntMap T is empty-preserving & IntMap T is universe-preserving ) by A2; :: thesis: verum