let S, T be non empty reflexive antisymmetric RelStr ; :: thesis: UPS (id S),(id T) = id (UPS S,T)
A1: dom (UPS (id S),(id T)) = the carrier of (UPS S,T) by FUNCT_2:def 1;
for x being set st x in the carrier of (UPS S,T) holds
(UPS (id S),(id T)) . x = x

proof

let x be set ; :: thesis: ( x in the carrier of (UPS S,T) implies (UPS (id S),(id T)) . x = x )
assume x in the carrier of (UPS S,T) ; :: thesis: (UPS (id S),(id T)) . x = x
then reconsider f = x as directed-sups-preserving Function of S,T by Def4;
(UPS (id S),(id T)) . f = ((id T) * f) * (id S) by Def5
.= f * (id S) by FUNCT_2:23 ;
hence (UPS (id S),(id T)) . x = x by FUNCT_2:23; :: thesis: verum

end;

hence UPS (id S),(id T) = id (UPS S,T) by A1, FUNCT_1:34; :: thesis: verum