let R, S, T be Ring; ( R,S are_isomorphic & S,T are_isomorphic implies R,T are_isomorphic )
assume A1:
( R,S are_isomorphic & S,T are_isomorphic )
; R,T are_isomorphic
then consider f being Function of R,S such that
A2:
f is isomorphism
;
consider g being Function of S,T such that
A3:
g is isomorphism
by A1;
( g * f is one-to-one & g * f is onto )
by A2, A3, FUNCT_2:27;
hence
R,T are_isomorphic
by A2, A3; verum