let S, T be non empty up-complete Poset; :: thesis: for f being Function of S,T holds
( f is isomorphic iff Sigma f is isomorphic )
let f be Function of S,T; :: thesis: ( f is isomorphic iff Sigma f is isomorphic )
( RelStr(# the carrier of (Sigma S), the InternalRel of (Sigma S) #) = RelStr(# the carrier of S, the InternalRel of S #) & RelStr(# the carrier of (Sigma T), the InternalRel of (Sigma T) #) = RelStr(# the carrier of T, the InternalRel of T #) ) by YELLOW_9:def 4;
hence ( f is isomorphic iff Sigma f is isomorphic ) by Th5; :: thesis: verum